Formaliser les mathématiques avec Lean et IA

Il y a dix ans, écrire une preuve formelle en Lean ou en Coq demandait un effort immense, réservé à des spécialistes patients. Chaque lemme exigeait des heures de travail manuel, sans aide extérieure. Aujourd'hui, l'IA a changé la donne : les assistants fondés sur des modèles et des agents aident à proposer des étapes, à compléter des démonstrations et à gérer des tokens de raisonnement. Dr. Samuel Allen Alexander raconte cette bascule et montre comment un prompt bien choisi permet désormais d'avancer vite là où l'on restait bloqué.

Le texte commenté réunit sept auteurs, dont Kevin Buzzard, figure connue de la formalisation. Buzzard a obtenu environ un million de livres sterling et cinq ans pour formaliser le dernier théorème de Fermat. Le projet illustre une ambition nouvelle : démontrer qu'une grande preuve classique peut vivre dans un assistant moderne. Pourtant, la vidéo souligne que les grands laboratoires ont avancé promptement, avec des systèmes d'IA qui produisent des résultats utiles avant même la fin des chantiers académiques.

OpenAI a surpris la communauté en publiant d'un coup près de quatre cents familles de résultats, avec énoncés, preuves et traces exploitables. Cette masse rend possible un usage par le bas : chacun peut reprendre un lemme, le tester dans Lean, l'adapter à son besoin. L'agent ne remplace pas le mathématicien, mais il fournit des suggestions, des tokens intermédiaires et des prompts réutilisables. Un modèle entraîné sur ce fonds devient un collègue disponible, qui aide à explorer vite des variantes et à consolider la base commune.

Les auteurs du texte redoutent un scénario sombre : un corpus médiocre ferait perdre du temps et des fonds, laisserait des bibliothèques inutilisées, fragiliserait les normes de rigueur et retarderait le domaine de plusieurs décennies. Ils plaident pour une coordination stricte avant toute production massive. L'orateur se montre peu convaincu par ce pessimisme. Selon lui, multiplier les essais imparfaits reste fécond, car la critique collective corrige les erreurs et les bons fragments survivent dans la bibliothèque partagée.

Deux succès récents montrent le potentiel concret. OpenAI a aidé à traiter la conjecture de la distance unitaire, avec des idées neuves sur des configurations de points. De son côté, la page recherche d'Anthropic décrit une nette progression sur la densité des zéros de la fonction zêta de Riemann, passée de 41,6 pour cent à 67,2 pour cent grâce à l'aide de Claude. Ces exemples prouvent qu'un agent bien guidé, nourri de prompts précis et de tokens de calcul, peut soutenir une recherche vivante et non se limiter à vérifier l'existant.

Tout vérifier a un prix, rappellent les auteurs. Si chaque détail devient lisible par un système, le lecteur humain peut perdre le fil de l'idée, le partage du crédit devient flou et la charge de travail augmente pour maintenir l'ensemble. Une prépublication déposée sur arXiv montre déjà cette tension : la preuve existe, mais son sens reste à expliquer. L'IA, avec ses modèles et ses agents, aide à produire, puis il faut encore enseigner, attribuer les mérites et rendre le texte accessible aux étudiants.

Face à ces craintes, l'orateur défend les formalisateurs de garage, ces passionnés qui travaillent hors des grandes équipes. Il met en garde contre des gardiens élitistes qui voudraient filtrer chaque contribution au nom de la pureté. Les mathématiques, dit-il, ne sont pas fragiles : elles forment un royaume platonicien solide, où une erreur locale ne détruit pas l'édifice. Un prompt maladroit ou un token erroné se repère et se corrige. Mieux vaut laisser chacun essayer, publier, discuter, puis améliorer.

Le trio gagnant associe Lean, la collection Mathlib et l'IA. Lean offre un langage de preuve dont la justesse se vérifie comme avec un compilateur : chaque pas doit satisfaire le système, sans exception. Mathlib fournit une bibliothèque vaste et structurée, que les modèles peuvent interroger et enrichir. Le site Lean Lang présente cette alliance comme le socle de l'avenir, où un agent propose, où Claude critique, où le noyau valide. Le savoir-faire formel devient ainsi transmissible, testable et cumulable par toute la communauté.

Le projet Tau Ceti illustre cette méthode à grande échelle. Des humains écrivent des feuilles de route, l'IA rédige des ébauches de preuves, puis une revue contradictoire confronte les propositions avant validation. Une compilation permanente contrôle chaque ajout, en aval de Mathlib, pour garantir la cohérence de l'ensemble. Les pages TauCetiProject décrivent ce flux exigeant, tandis que le dépôt GitHub expose la bibliothèque produite par les agents. Le prompt initial humain cadre le travail, les tokens générés fournissent la matière, le système tranche.

La feuille de route Lean FRO pour l'année quatre, de septembre 2026 à février 2027, donne un cadre officiel à cet effort. Elle associe Tau Ceti, Hex et Palomar autour d'objectifs mesurables et d'une infrastructure partagée. Le site Lean Lang affirme que l'essentiel des mathématiques courantes sera utilisable sous trois ans dans cet écosystème vérifié. Un modèle aide à formaliser, un agent teste des variantes, Claude relit les passages délicats. Cette planification rend visible le chemin entre l'ambition affichée et le travail quotidien des équipes.

Les auteurs appellent à changer d'échelle : multiplier par dix l'effort autour de Tau Ceti et de Formal Frontier, avec des plans rédigés par des experts, des ateliers réguliers et des modèles de financement durables. Ils proposent un hébergement associatif pour la maintenance des bibliothèques et la formation des nouveaux venus. Un agent peut préparer les sessions, un modèle peut résumer les discussions, et les tokens échangés nourrissent la mémoire collective. L'objectif reste simple : passer de démonstrations isolées à une production continue et partagée.

Le titre promet une méthode, avec son How to qui annonce une technique applicable pas à pas. Or le texte propose surtout un appel à la gouvernance : qui décide, qui finance, qui valide et selon quelles normes. L'orateur regrette ce décalage et plaide pour l'honnêteté des étiquettes. Un appel à coordonner les fonds et les énergies ne doit pas se présenter comme un manuel. Les lecteurs méritent un intitulé qui reflète le propos, surtout quand l'IA et ses prompts occupent déjà une place centrale dans les débats.

La prévision finale tient en peu de mots : le connu de 2026 se referme vite, car des agents infatigables comblent les lacunes une à une. La frontière avance sans cesse, portée par des modèles plus habiles et des prompts mieux ajustés. L'écart entre l'informel et le formel s'amincit, rendant la vérification presque routinière. Reste à choisir ce que nous voulons démontrer ensuite, car la puissance disponible ne dit pas où chercher. L'avenir appartiendra à ceux qui posent les bonnes questions et qui osent explorer.