POINCARÉ, VÉRIFIÉ LIGNE À LIGNE PAR LA MACHINE

Vérifier une preuve est l’une des tâches les plus exigeantes des mathématiques, surtout quand un raisonnement traverse plusieurs domaines. À mesure que l’IA accélère la production de preuves, une vérification fiable compte davantage. Les assistants de preuve comme Lean 4 offrent une réponse : définitions, énoncés et preuves s’écrivent comme du code, et un petit cœur de confiance du logiciel, son « noyau », vérifie chaque étape. Une preuve acceptée par le noyau établit son énoncé ; il reste aux humains à vérifier que l’énoncé dit bien ce que les mathématiciens veulent dire.

Une preuve condensée, une bibliothèque manquante

La conjecture de Poincaré, démontrée par Perelman, affirme que toute variété de dimension trois fermée et simplement connexe — en gros, un espace 3D fini sans trou où une boucle pourrait rester accrochée — équivaut à la sphère de dimension trois. La preuve suit le programme du flot de Ricci lancé par Richard Hamilton. Les trois prépublications de Perelman de 2002-2003 donnaient les arguments clés sous une forme très condensée ; des exposés détaillés ont suivi, dont la monographie de 2007 de John Morgan et Gang Tian, que suit ce projet.

Cette preuve repose sur une analyse géométrique qui manquait en grande partie à la bibliothèque communautaire de Lean, Mathlib. Une bonne partie des fondations a dû être construite de zéro.

Des jalons figés par les mathématiciens

Zhiyuan Zhang, Axel Delaval, Bin Dong, Chunlei Liu et leurs collègues de l’université de Pékin et d’autres institutions pékinoises ont commencé en mai 2026 : trois « ingénieurs IA » de formation mathématique, épaulés par des mathématiciens. Leur première approche — formaliser de gros pans de théorie de fond — s’est révélée lente, et le code produit ne répondait pas à leurs attentes.

En septembre 2026, ils sont repartis de zéro. La preuve a été découpée en environ 90 jalons, chacun étant un énoncé Lean précis accompagné des définitions nécessaires. Des mathématiciens ont relu ces énoncés avant ou pendant leur formalisation, puis ils ont été figés : les agents ne pouvaient pas les modifier, et toute correction repassait par les mathématiciens. Comme personne ne pouvait lire chaque ligne écrite par les agents, ces jalons sont devenus les points de contrôle où les humains vérifiaient les mathématiques.

Les agents ont ensuite travaillé en parallèle, via des sessions interactives avec des outils de programmation — surtout Codex et Claude Code — et via un système nommé Archon Horizon, qui répartit des « missions » bornées sur de nombreux serveurs. Un robot compilait chaque contribution et fusionnait celles qui étaient acceptées. GPT-6-Astra a porté l’essentiel de la formalisation des énoncés et de la construction des preuves ; Fable-5.1 a servi aux vérifications indépendantes, au diagnostic des tâches bloquées et à la relecture des énoncés.

2,8 millions de lignes en deux semaines environ

Après les mois de préparation, la formalisation principale a pris un peu plus de deux semaines. Abonnements à l’IA et serveurs loués ont coûté environ 25 000 dollars. Le résultat démontre les versions topologique et lisse du théorème, compile entièrement et passe une vérification indépendante face à des énoncés cibles écrits avec la seule Mathlib.

C’est gigantesque : environ 3,2 millions de lignes de Lean, réduites à 2,8 millions en ne gardant que ce dont dépend le théorème final. Selon le décompte des auteurs, près de la moitié relève de la théorie de fond. Un résultat classique que Morgan et Tian évoquent dans une simple note de bas de page — sur les structures lisses des variétés de dimension trois — a demandé à lui seul quelque 650 000 lignes.

Ce que les humains ont encore fait

Les auteurs rangent les obstacles en trois catégories : lacunes mathématiques, problèmes de mise en œuvre en Lean, problèmes de coordination. Les humains ont fixé la portée des énoncés (par exemple, quand restreindre un résultat à la dimension trois), repéré des arguments manquants — comme une étape de compacité locale que les agents ne trouvaient pas — et débusqué des hypothèses cachées. Leur principale leçon : l’organisation du travail a compté autant que les capacités des agents. Ils tirent la même conclusion de la récente formalisation du dernier théorème de Fermat par Anthropic, qui avait elle aussi dû redémarrer après des premiers essais où les agents perdaient le fil du projet.

Vérifié, mais pas encore rangé

Les auteurs ne considèrent pas le travail comme terminé. Le code regorge de doublons ; les preuves des agents ne suivent pas toujours la route de référence ; et en faire une bibliothèque réutilisable d’analyse géométrique est la prochaine étape. Une formalisation indépendante de la même conjecture par une autre équipe a aussi été annoncée. Leur espoir : qu’un jour, un mathématicien seul puisse vérifier ses propres recherches avec de tels outils.

Conflit d’intérêts. L’équipe a utilisé Claude Code et le modèle Fable-5.1, tous deux d’Anthropic, aux côtés de GPT-6-Astra, utilisé via des abonnements OpenAI, qui a fait l’essentiel du travail. L’article compare aussi son projet à la formalisation du dernier théorème de Fermat par Anthropic. Cet article est écrit par Claude.