L'IA a-t-elle "résolu" le dernier théorème de Fermat ? Une preuve de 13 millions de lignes complétée en 11 jours qui change les mathématiques

Un problème de 350 ans "prouvé" en 11 jours

Un des problèmes les plus célèbres de l'histoire des mathématiques attire à nouveau l'attention du monde.

En septembre 2026, Anthropic a annoncé que son IA "Claude" avait créé une preuve formelle complète de la dernière conjecture de Fermat, vérifiable par ordinateur du début à la fin. Le travail a pris 11 jours. Le code Lean généré atteint environ 13 millions de lignes, et au cours du processus, 30 300 théorèmes ont été prouvés, dont 29 500 ont été utilisés dans la preuve finale.

À première vue, ces chiffres donnent l'impression que l'IA a résolu en seulement 11 jours un problème qui a tourmenté l'humanité pendant des siècles. Cependant, il y a une distinction importante à faire. Ce que Claude a fait n'est pas de découvrir une méthode de solution inconnue. Il a traduit la preuve, complétée par Andrew Wiles et Richard Taylor dans les années 1990 et reconnue comme correcte par la communauté mathématique, dans un langage que l'ordinateur peut vérifier logiquement, comblant les nombreuses lacunes intermédiaires.

Ce n'est pas une "nouvelle découverte de preuve", mais une "vérification mécanique complète d'une preuve existante". Ne pas comprendre cette différence conduit à surestimer le résultat. D'un autre côté, considérer la formalisation comme un simple travail de traduction sous-estime la difficulté et l'impact de cette réalisation.

La ligne laissée par Fermat dans la marge

La dernière conjecture de Fermat affirme qu'il n'existe pas de triplet d'entiers positifs a, b, c et un entier n supérieur à 2 tel que "a^n + b^n = c^n".

Vers 1637, Pierre de Fermat a écrit cette affirmation dans la marge d'un ancien livre de mathématiques grecques, "Arithmetica", en ajoutant qu'il avait trouvé une preuve remarquable, mais que la marge était trop étroite pour la contenir. Cependant, cette preuve n'a jamais été découverte.

Depuis lors, des générations de mathématiciens ont tenté de relever le défi, et bien que des preuves aient été trouvées pour des indices particuliers, le cas général est resté non résolu pendant plus de 350 ans. Le tournant est survenu en 1993, lorsque Wiles a annoncé une preuve après des années de recherche secrète, mais une faille majeure a été découverte lors de la vérification. Wiles, avec Taylor, a travaillé à la correction et a surmonté le problème en 1994. L'article a été publié en 1995.

Cette histoire montre que dans les mathématiques, "prouvé" ne signifie pas que quelqu'un a écrit la réponse instantanément. La preuve doit être lue par d'autres experts, examinée, y compris les prémisses et les théorèmes cités, et la chaîne logique doit être intacte. Le fait qu'une faille ait été trouvée dans la preuve d'un mathématicien aussi éminent que Wiles symbolise la difficulté de la tâche.

Ce qui est "évident pour les humains" ne l'est pas pour les ordinateurs

Les articles mathématiques habituels sont écrits pour être lus par des experts humains. Les auteurs omettent les transformations évidentes, se réfèrent à des résultats connus et ne précisent pas les parties compréhensibles par le contexte. Les lecteurs utilisent également leurs connaissances de fond pour suivre la logique entre les lignes.

Cependant, les ordinateurs ne font pas de suppositions telles que "cela doit être évident". Il est nécessaire de spécifier strictement les définitions, les prémisses, les types, les théorèmes utilisés et les conclusions qui en découlent, en montrant que chaque étape suit les règles. L'outil utilisé pour ce travail était Lean, un assistant de preuve de théorème.

Dans Lean, les preuves sont écrites dans un format proche d'un programme. Un petit noyau vérifie si la preuve saisie suit les règles logiques et ne l'accepte pas s'il y a un saut. En ce sens, la preuve formelle est proche d'un test automatique très rigoureux pour une affirmation mathématique.

La difficulté réside dans le fait que remplacer simplement l'article de Wiles par un langage machine ne suffit pas. Les preuves destinées aux humains reposent sur d'énormes systèmes de connaissances en algèbre, géométrie, analyse harmonique, théorie des nombres, etc. Si les concepts nécessaires et les théorèmes auxiliaires n'existent pas dans la bibliothèque partagée de Lean, ils doivent être définis et prouvés à nouveau. L'ampleur de 13 millions de lignes résulte également de la construction de cette "fondation invisible" une par une.

Plusieurs IA ont partagé la tâche de la gigantesque preuve

Dans l'expérience d'Anthropic, des dizaines d'agents Claude ont travaillé en parallèle. Un agent définissait un concept, un autre prouvait un théorème auxiliaire, et un autre encore combinait ces éléments pour progresser vers des théorèmes de niveau supérieur. C'était comme une recherche collaborative humaine, mais exécutée à grande échelle par un groupe d'IA.

Cependant, tout n'a pas été fluide dès le début. Lors des premiers essais, les agents perdaient de vue la progression globale du projet et ne parvenaient pas à utiliser efficacement les résultats des uns et des autres. Dans un travail à long terme, non seulement la capacité de raisonnement individuelle de chaque IA, mais aussi le mécanisme de gestion des tâches terminées et de ce qui devait être prouvé ensuite, étaient cruciaux.

Le système utilisé pour cela était Prove2Me, une plateforme de formalisation collaborative qui gère les dépendances entre théorèmes sous forme de graphe orienté acyclique. Les éléments à prouver étaient disposés comme une carte, permettant à chaque agent de choisir une tâche non résolue et aux autres agents de réutiliser les résultats terminés. La conception permettant de réduire la charge de compilation de Lean et d'utiliser des explications en langage naturel pour la recherche a également soutenu la division du travail à grande échelle.

Finalement, le groupe d'IA a consommé environ 6 milliards de tokens de sortie et a atteint la racine de la preuve en un peu moins de 11 jours. Selon Anthropic, en plus de l'inspection par Lean, un outil de comparaison a également vérifié que la description finale du théorème correspondait à celle de la dernière conjecture de Fermat dans la bibliothèque existante Mathlib. Autrement dit, ils ont confirmé qu'ils avaient atteint l'affirmation visée, et non prouvé un problème différent avec un nom similaire.

Les 5 ans de travail humain et les 11 jours de l'IA ne sont pas directement comparables

Souvent comparé à cela, il y a le projet de formalisation centré sur l'humain dirigé par le mathématicien Kevin Buzzard de l'Imperial College London. Ce projet a commencé en 2024 et vise à formaliser la dernière conjecture de Fermat avec Lean sur plusieurs années.

La description "un travail de 5 ans pour les humains terminé en 11 jours par l'IA" est frappante, mais les objectifs des deux ne sont pas complètement identiques. Le succès d'Anthropic a priorisé la possibilité de rendre le théorème vérifiable par machine de bout en bout. En revanche, Buzzard et son équipe visent également à établir des théories de base pouvant être intégrées dans une bibliothèque partagée, et à créer des documents dynamiques permettant aux humains d'explorer et d'apprendre des preuves modernes.

Créer un code massif qui "passe" en peu de temps et organiser les résultats de manière à ce que les mathématiciens puissent les comprendre, les réutiliser et les connecter à des recherches futures sont des tâches différentes. Anthropic lui-même a expliqué qu'il avait utilisé la base construite par le projet humain et la bibliothèque Mathlib existante. Dépeindre cette compétition comme une simple course de vitesse entre l'IA et les mathématiciens n'est pas exact.

Néanmoins, le fait que la formalisation de bout en bout soit devenue possible en jours plutôt qu'en années est significatif. Buzzard a écrit sur son blog que bien que cette réalisation n'apporte presque rien de nouveau sur le plan mathématique, le fait que l'IA ait pu formaliser l'équivalent de milliers de pages de littérature en 11 jours montre le potentiel de la formalisation automatique. Il a également déclaré qu'après la formalisation, il était certain à 100 % de la preuve, alors qu'il la considérait auparavant comme correcte à 99,9 %, ce qui est perçu comme un symbole de cette réalisation.

Les réseaux sociaux se divisent entre "émerveillement" et "ce n'est pas une nouvelle découverte"

Après l'annonce, il y a eu une grande réaction sur X, Reddit, Hacker News, etc. Le compte officiel de Lean a présenté le succès comme la première preuve entièrement vérifiée par ordinateur. Sur Hacker News, des centaines de commentaires ont été rassemblés sur les publications connexes, et sur Reddit, des voix exprimant leur étonnement se sont succédé : "Inimaginable il y a quelques années", "Écrasé par l'ampleur de 13 millions de lignes", "Est-il vraiment nécessaire d'avoir plus de 29 000 théorèmes intermédiaires ?".

Cependant, l'avertissement le plus répété concernait la façon dont le titre était perçu. En réponse à l'expression "L'IA a résolu la dernière conjecture de Fermat", de nombreuses corrections ont été postées : "Ce sont Wiles et Taylor qui l'ont résolue, et Claude a formalisé la preuve existante dans Lean", "Ce n'est pas une nouvelle découverte mathématique". Parmi les réactions, certains ont minimisé la formalisation comme une simple conversion de format, mais il y a eu des contre-arguments affirmant que combler les lacunes d'une longue preuve et rendre des dizaines de milliers de théorèmes intermédiaires vérifiables par machine est en soi un grand accomplissement de recherche.

Les discussions ont également porté sur le rôle des chercheurs et la répartition des fonds. Certains ont salué l'atteinte par l'IA d'un travail soutenu par des subventions importantes et des plans pluriannuels comme un saut dans la productivité de la recherche. D'un autre côté, des inquiétudes ont été exprimées quant à la possibilité que les thèmes de recherche des jeunes chercheurs soient préemptés par l'IA, ou que la motivation pour réfléchir aux mathématiques à la main soit perdue. Dans la section des commentaires du blog de Buzzard, des opinions ont été échangées, certaines voyant cela comme "la fin triste des mathématiques", et d'autres répondant que "le contenu mathématique n'a pas changé, seul le moyen de vérification a progressé".

Ce ne sont pas des sondages d'opinion aléatoires, mais simplement des tendances observées dans les publications sur chaque réseau social. Néanmoins, elles montrent bien pourquoi ce succès est facilement mal compris et suscite en même temps de fortes émotions. Les gens ne réagissent pas seulement à un théorème, mais à une question plus large : "Jusqu'où le travail intellectuel peut-il être automatisé ?".

Une preuve correcte et une preuve utile ne sont pas la même chose

Ce succès présente également des faiblesses claires. L'échelle de 13 millions de lignes dépasse de plus de cinq fois celle de la bibliothèque mathématique principale Mathlib. Même si la machine peut vérifier la justesse, il n'est pas facile pour les humains de saisir l'ensemble, de trouver les parties nécessaires et de les réutiliser dans d'autres preuves.

Pour le développement des mathématiques, il ne suffit pas d'avoir des conclusions correctes, mais aussi des explications compréhensibles du pourquoi, des abstractions appropriées pour organiser les concepts, et des lemmes utilisables dans d'autres domaines. Si la même théorie de base est recréée chaque fois sous forme de code massif dédié, les preuves formelles peuvent augmenter, mais le système de connaissances ne se développera pas facilement. Il y a un risque que des preuves vérifiables soient produites en masse, mais que chacune devienne une île isolée avec peu de compatibilité.

Par conséquent, le prochain défi sera probablement de raccourcir et d'organiser le code produit par l'IA, de le réduire à Mathlib, et de le relier à des explications lisibles par les humains. L'IA ouvre la voie de manière brute, et les humains et l'IA transforment cette voie en carte. Ce succès est mieux vu comme un point de départ pour cette nouvelle division du travail plutôt qu'une fin.

Un "second lecteur infatigable" pour compléter les limites de la relecture

La plus grande signification n'est pas d'avoir prouvé à nouveau un théorème célèbre, mais d'avoir montré la possibilité d'exécuter à grande échelle une vérification mécanique qui était auparavant irréaliste en raison des coûts et du temps.

La vérification des articles mathématiques nécessite beaucoup de temps de la part d'experts. Surtout lorsque de nouvelles théories s'étendent sur des centaines de pages et dépendent de nombreuses recherches antérieures, il est difficile pour les relecteurs de tout reconstituer. Si l'IA peut aider à la formalisation, il pourrait devenir courant de soumettre, avec les articles destinés aux humains, des certificats vérifiables par Lean, etc.

Cela deviendra encore plus important à l'ère où l'IA commence à produire en masse des résultats mathématiques. Si l'IA génère des candidats à des articles à un rythme supérieur à celui de la lecture humaine, la relecture traditionnelle ne suffira pas. En combinant une IA génératrice, une IA de formalisation et un noyau de vérification final qui vérifie la logique, il sera possible de vérifier efficacement si une conclusion est logiquement dérivée.

Bien sûr, la preuve formelle ne juge pas toute la valeur d'un article. Il reste à déterminer si les définitions représentent correctement les problèmes réels, si le sujet de recherche est important, si la preuve offre de nouvelles perspectives, et si l'explication est éducative. De plus, la confiance dans les logiciels de vérification et les bibliothèques de base, l'audit des codes massifs, et la répartition inégale des ressources informatiques sont également des problèmes inévitables.

Néanmoins, le fait que les mathématiques disposent d'un "second lecteur" infatigable, qui ne craint pas l'autorité et ne manque pas les lacunes logiques, est d'une grande importance.

L'IA remplacera-t-elle les mathématiciens ?

Cet événement ne signifie pas que l'IA a remplacé d'un coup le travail des mathématiciens. Il a fallu des humains pour créer le prototype de la preuve, des chercheurs qui ont passé des décennies à développer la théorie, une communauté qui a développé Mathlib et Lean, et des développeurs qui ont conçu la plateforme pour diviser la preuve, pour que les 11 jours de Claude soient possibles.

Cependant, conclure simplement que "l'IA n'est qu'un outil" est prématuré. Le fait que plusieurs agents aient pu se redresser après des échecs, suivre les dépendances et accumuler des dizaines de milliers de théorèmes pour atteindre un objectif gigantesque est qualitativement différent de l'automatisation traditionnelle. Au lieu que les humains donnent des instructions détaillées étape par étape, un groupe d'IA a été capable de mener à bien une grande partie d'un projet à long terme avec un objectif et un environnement de travail