Claude a bouclé Fermat en 11 jours : 13,4 millions de lignes de Lean et pas un seul « évidemment »

Le 4 septembre, Anthropic a présenté le tout premier test machine complet du dernier théorème de Fermat. Claude en 11 jours, presque sans l'aide de personnes, a traduit la preuve d'Andrew Wiles dans le langage Lean : 13,4 millions de lignes de code, environ 30 000 théorèmes intermédiaires, zéro « évident d'après ce qui a été dit ». Le projet, que les mathématiciens préparaient depuis des années - seul le dessin de la première phase de Kevin Buzzard de l'Imperial College de Londres faisait 86 pages - a été achevé en une semaine et demie.

Précisons immédiatement ce qui n'est pas ici : il n'y a aucune nouvelle preuve. Le modèle n’a pas proposé sa propre voie vers le théorème. Elle a fait quelque chose de différent et, franchement, non moins complexe - elle a pris une preuve humaine, où sur chaque page il y a des avertissements comme "cela suit de manière triviale", et l'a réécrite pour que le compilateur vérifie chaque étape. Après 1995, les mathématiciens avaient confiance dans le théorème à 99,9 %. Maintenant, vous pouvez y aller à cent pour cent : Lean a parcouru toute la dérivation des trois axiomes standards, et il n'y a plus rien à douter.

Qu’est-ce que l’ordinateur a vérifié exactement ?

Les chiffres sont ici plus appropriés que les épithètes.

• Les 13,4 millions de lignes de Lean sont plus de cinq fois plus grandes que l'ensemble de Mathlib, la principale bibliothèque mathématique formelle du système.
• Environ 30 000 théorèmes intermédiaires ont été prouvés ; la production finale impliquait environ 29 500 personnes.
• La compilation d'un référentiel sur une machine à 96 cœurs prend environ 20 fois plus de temps que la compilation de Mathlib. Buzzard a reçu un serveur avec 500 Go de RAM pour la durée du test.
• On ne s'appuie que sur trois axiomes standards Lean. Pas d’hypothèses de simplicité.

Kevin Buzzard, le même mathématicien qui dirige le projet de formalisation Fermat pour la communauté depuis 2024, a téléchargé le référentiel, l'a assemblé et a exécuté le comparateur : la formulation de sortie du théorème coïncide avec celle de référence de Mathlib, toutes les cases sont vertes. Son bilan : « une réalisation extraordinaire d’auto-formalisation ».

Une ligne en marge, trois siècles et demi de travail

Vers 1637, Pierre de Fermat attribue l'énoncé en marge de l'Arithmétique de Diophante : pour n supérieur à deux, l'équation aⁿ + bⁿ = cⁿ n'a pas de solutions en nombres naturels. Ci-dessous se trouve une phrase devenue légende : « J’ai trouvé une preuve vraiment merveilleuse, mais les marges sont trop étroites pour cela. » Des générations de mathématiciens, d’Euler à Kummer, ont progressé progressivement vers ce résultat. En 1908, un prix de 100 000 marks-or fut décerné pour preuve et la première année, 621 solutions incorrectes furent reçues.

En juin 1993, Andrew Wiles a présenté sa preuve lors d'une série de conférences à Cambridge. Deux mois plus tard, un critique a posé une question révélant un trou dans l’un des modèles. Pendant un an, Wiles l'a réparé - d'abord seul, puis avec son ancien élève Richard Taylor - était sur le point de tout abandonner et, en 1995, il a publié un texte de 129 pages. Restait la dernière question « d’ingénierie » : est-il possible de forcer l’ordinateur à confirmer tout cela dans son intégralité ?

Pas une nouvelle preuve, mais une nouvelle opportunité

Il est basé sur l'analyse de Darmon, Diamond et Taylor en 1995 de l'argument de Wiles-Taylor à travers le théorème de Langlands-Tunnell et la descente de niveau de Ribet. L'idée de formaliser Wiles a été exprimée dans les années 2000 par l'informaticien néerlandais Jan Bergstra, mais jusqu'à récemment, cela était considéré comme un travail pour toute une direction scientifique. Les cas individuels - quatrième degré, simples et réguliers - ont été déplacés plus tôt vers le Lean. Avec le nouveau référentiel, la liste complète des 100 tâches de formalisation de Weidik est close : le référentiel auquel ce domaine a été comparé a vingt ans.

Buzzard, d'ailleurs, écrit honnêtement : mathématiquement, le travail ne révèle rien de nouveau - il croyait déjà en Wiles. La valeur est ailleurs. La révision d’un nouvel article en mathématiques prend des mois, voire des années ; Si l’on peut demander à une machine de formaliser une preuve à la volée, l’évaluation par les pairs diminuera et des hypothèses cachées au niveau expert commenceront à faire surface. Pour la science, où tout repose sur l’honnêteté des conclusions, il s’agit d’un changement sérieux.

À quoi ressemblaient ces 11 jours de l’intérieur

Les travaux ont été dirigés par Tianyi Peng, un chercheur d'Anthropic qui avait auparavant constitué un groupe d'outils de formalisation de l'IA à l'Université de Columbia. Selon lui, il n’avait initialement pas prévu d’aller au bout : il voulait seulement voir à quel point Claude ferait avancer le projet de Buzzard. Promu en finale.

De nombreux agents ont travaillé en parallèle : certains ont complété des définitions mathématiques, d’autres ont pris d’assaut des lemmes intermédiaires, d’autres ont remonté l’arbre des théorèmes et d’autres encore ont rassemblé les parties en une seule conclusion. Les premiers jours se sont mal passés : les agents ont perdu la vision globale du projet et environ sept pour cent des premières tentatives sont restées dans le code final. Le revirement s'est produit lorsque l'équipe a été transférée sur la plateforme Prove2Me : la preuve qu'elle contient est un graphique de nœuds de théorème, où vous pouvez voir ce qui a déjà été prouvé, ce qui attend les prérequis et ce qu'il faut prendre ensuite. Les déclarations sont séparées des preuves, la compilation est accélérée et chaque théorème a une description textuelle consultable. L'ampleur du travail est d'environ six milliards de jetons de production, et les invites humaines ont été réduites à un niveau élevé : « cette direction est une priorité ».

Où regarder

Le référentiel est publié sur GitHub - si vous le souhaitez, vous pouvez exécuter la vérification vous-même si vous disposez d'une machine avec 96 cœurs et des nerfs solides. Sources primaires : analyse d’Anthropic Et Le message de Buzzard sur le blog du projet Xena.

Et si, après une histoire de 13 millions de lignes, vous voulez voir comment les modèles modernes gèrent des tâches plus petites - algorithmes, code, calculs - jetez un œil aux sections "Code" Et "Chat" le NeuralSpace : vous pouvez y expérimenter des modèles et les connecter à vos projets via l'API.