A Formalization of the Mean-Field Derivation of the Vlasov Equation: AI-Assisted Lean Formalization as a Strategy Game

Résumé Technique : Une formalisation de la dérivation de l'équation de Vlasov par champ moyen

Énoncé du problème
L'article traite du défi consistant à formaliser des résultats mathématiques complexes et de niveau recherche dans l'assistant de preuve Lean 4. Historiquement, la formalisation a pris du retard sur la découverte mathématique en raison de la nature laborieuse de la traduction d'arguments informels en code vérifiable par machine, de l'adaptation aux conventions des bibliothèques existantes et du comblement des lacunes des bibliothèques actuelles (Mathlib). Bien que les systèmes d'IA récents puissent générer rapidement des preuves en Lean, deux questions critiques subsistent : (1) Peut-on faire confiance à des preuves générées par un agent que l'on n'a pas écrit ? et (2) Le code résultant produit-il des mathématiques réutilisables, ou s'agit-il d'un « glue » jetable spécifique à un seul problème ?

Méthodologie : Le jeu de la formalisation
Les auteurs présentent le processus de formalisation comme un « jeu » avec des règles précises, séparant les rôles du mathématicien humain (le directeur) et de l'agent d'IA (l'exécuteur). La méthodologie est structurée en trois phases :

1. Phase initiale (Délimitation définitionnelle) : Le mathématicien humain traduit les théorèmes cibles et leurs définitions sous-jacentes en Lean, en laissant les preuves sous forme de sorry. L'objectif est de « verrouiller » l'API (signatures et définitions) avant de prouver quoi que ce soit. Cela empêche les erreurs de définition (par exemple, des classes de régularité ou des espaces métriques incorrects) de se propager dans l'ensemble du développement.
2. Phase intermédiaire (Pilotage de la décomposition) : L'humain dirige l'IA pour décomposer de grands théorèmes impossibles à prouver en sous-lemmes plus petits et maniables. L'IA exécute les preuves de ces sous-lemmes. Le rôle critique de l'humain est le « pilotage » : décider où couper un théorème, quel chemin mathématique la bibliothèque peut supporter, et quand abandonner une stratégie défaillante.
3. Phase finale (Triage des lacunes de la bibliothèque) : Les sorry restants sont triés. Ils sont classés comme :
   • Fantômes : Lacunes apparentes qui se dissipent à une lecture plus attentive des exigences.
   • Lacunes réelles à construire : Mathématiques standards manquantes de la bibliothèque, que l'équipe formalise à partir de primitives.
   • Lacunes réelles à différer : Véritables lacunes mathématiques marquées par des placeholders explicites (théorèmes cités) plutôt que construites, si elles ne sont pas essentielles au résultat central.

Conditions de victoire et réutilisabilité
L'article introduit deux critères vérifiables par machine pour valider le travail :

• La condition de victoire : Le développement compile sans sorry, et la commande #print axioms confirme que les théorèmes cibles dépendent uniquement des axiomes fondamentaux de Lean (propext, Classical.choice, Quot.sound). Cela certifie la validité de la preuve par rapport à l'énoncé écrit.
• La couche auto-contenue : Un sous-ensemble du développement est extrait et contient des mathématiques générales réutilisables par la bibliothèque plus large. Cette couche doit passer quatre tests :
  1. Isolation : Aucune dépendance ne court de la couche générale vers le code spécifique au problème (le compte de bord reversé est de 0).
  2. Compilation autonome : La couche compile contre Mathlib seule, sans import spécifique au problème.
  3. Propreté du linter : Le code passe la suite de linters automatisés de la bibliothèque avec zéro avertissement.
  4. Non-redondance : Aucune déclaration ne réitère des résultats déjà présents dans la bibliothèque.

Contributions clés et résultats
L'étude de cas formalise la dérivation de Dobrushin de l'équation de Vlasov non linéaire à partir de la dynamique hamiltonienne à $N$ particules. La formalisation couvre :

• Le caractère bien posé : Existence et unicité des solutions pour l'équation de Vlasov non linéaire.
• La stabilité : L'estimation de stabilité de Dobrushin dans la métrique de Wasserstein-1 ($W_1$).
• La limite de champ moyen : La convergence de la mesure empirique de $N$ particules vers la solution de Vlasov.
• Le principe de superposition : Un résultat à fenêtre courte montrant que les solutions faibles sont lagrangiennes (transportées par des flux de caractéristiques), nécessitant une hypothèse de régularité supplémentaire (potentiel $C^2$).

Résultats techniques spécifiques :

• Machinerie du transport optimal : Le build a généré une couche auto-contenue de mathématiques de transport optimal (49 déclarations, interface de 22 déclarations) incluant la métrique $W_1$ sous ses formes primale (couplage) et duale (Kantorovich–Rubinstein), ainsi que le pont de dualité entre elles. Cette couche compile contre Mathlib seule.
• Division du travail Humain-IA : Le mathémien humain n'a pas écrit de preuves mais a dirigé la stratégie. Les interventions humaines clés incluaient :
  • La correction d'un « effondrement silencieux » dans la classe de test des solutions faibles (où une définition de $C^\infty$ était en fait $C^\omega$, rendant la classe de test vide).
  • Le pilotage de la preuve de la dualité Kantorovich–Rubinstein en rejetant les approches d'espaces de Hilbert et en guidant l'agent vers le lemme de Farkas et la séparation géométrique.
  • La redirection de la preuve de stabilité de la formulation duale (nécessitant un théorème d'atteinte non prouvé) vers la formulation de couplage originale de Dobrushin, que la bibliothèque pouvait supporter.
  • La décision que le principe de superposition nécessite une régularité $C^2$ (AssW2) pour garantir que le flux de caractéristique est $C^1$, une nuance extraite de la prose et encodée dans une typeclass.
• Calendrier et coût : Les résultats de bien-posé et de stabilité ont été terminés en environ une semaine ; le développement complet (incluant le principe de superposition) a pris environ un mois. Le coût était d'environ 200 $ (un abonnement à taux fixe), sans codage manuel en Lean par l'humain.

Signification et affirmations
L'article affirme que ce modèle de « directeur stratégique » permet à la formalisation de suivre le rythme du travail mathématique ordinaire.

• Confiance : La confiance n'est pas établie par la lecture de chaque ligne de preuve par l'humain, mais par la condition de victoire vérifiable par machine (empreinte des axiomes) et la supervision par l'humain des définitions et de la stratégie de décomposition.
• Réutilisabilité : Le travail démontre que la formalisation assistée par IA peut produire des mathématiques « absorbables » (la couche auto-contenue) plutôt que du code jetable.
• Pérennité méthodologique : Le cadre du « jeu » est conçu pour survivre à des outils d'IA spécifiques. Les règles (conditions de victoire, phases, cadre de stratégie) sont indépendantes de l'outil. L'article soutient que bien que les agents d'IA et les bibliothèques spécifiques évoluent, la division du travail — où l'humain fournit le jugement mathématique et la machine la l'exécution — reste une stratégie viable et scalable.
• Limites : Les auteurs se montrent modestes, notant que le contrôle de la « couche auto-contenue » a été appliqué à un seul projet et que la couche extraite importe toujours Mathlib dans son ensemble plutôt que de manière minimale. Le délai est une observation unique dépendant de la fluidité du directeur humain. L'article ne prétend pas résoudre le cas de la force « singulière » (ex: gravité) mais se concentre sur le cas lisse où des bibliothèques réutilisables peuvent être construites.

L'article conclut que le « métier » de la formalisation est en train de passer de l'écriture de preuves à la direction d'agents, gérant le « répertoire de mouvements » (heuristiques, stratégies de décomposition et triage de bibliothèque) qui permettent de certifier l'analyse complexe.