Assistant de preuve Lean et IA : comment les démonstrations deviennent vérifiables par machine

Onze jours, un essaim d'agents, 13 millions de lignes de code : une IA a rendu la démonstration du dernier théorème de Fermat vérifiable par machine. Ce qui a compté, ce n'est pas tant la puissance de calcul qu'un vérificateur qui ne laisse passer aucune erreur.

Vers 1637, Pierre de Fermat a noté en marge d'un livre une affirmation dont il prétendait détenir la preuve. On ne l'a jamais retrouvée. Il a fallu attendre 1995 pour qu'Andrew Wiles publie une démonstration complète. Le 4 septembre 2026, Anthropic a annoncé qu'un essaim d'agents Claude avait formalisé intégralement cette démonstration dans le langage de preuve Lean. C'est l'assistant de preuve Lean, qui vérifie chaque étape d'une démonstration par machine, qui l'a rendu possible.

Cet article remet cette annonce en perspective. Il explique ce qu'est un assistant de preuve et pourquoi un résultat issu de Lean est jugé fiable. Il décrit comment les agents ont travaillé ensemble et situe l'annonce parmi les problèmes d'olympiade et les problèmes d'Erdős. Il distingue les chiffres étayés, les déclarations du constructeur et les questions ouvertes. La thèse : la nouveauté ne tient pas seulement au fait qu'une IA fasse des mathématiques. Elle tient à l'association d'un modèle libre d'essayer et d'un programme qui valide chaque étape sans complaisance.

Le dernier théorème de Fermat : ce qu'Anthropic a réellement annoncé

Le théorème affirme que l'équation aⁿ + bⁿ = cⁿ n'a aucune solution en nombres entiers strictement positifs pour un exposant n supérieur à 2. L'énoncé se comprend facilement et il est resté extrêmement difficile à démontrer pendant des siècles. En 1908, un prix de 100 000 marks-or a été promis et, selon Anthropic, 621 fausses démonstrations ont été envoyées la première année. Wiles a présenté une preuve en 1993, y a trouvé une faille et l'a comblée avec Richard Taylor. La publication a suivi en mai 1995.

La dernière annonce porte sur le degré de certitude de cette preuve lorsqu'une machine vérifie chaque étape. Les principales indications de la publication d'Anthropic figurent dans le tableau.

Un token est ici un petit morceau de texte produit par un modèle de langage, par exemple un fragment de mot. La source n'indique aucun coût financier. Toutes les données viennent du constructeur et n'ont pas été recomptées de façon indépendante.

La distinction est importante. Il s'agit d'une formalisation, pas d'une nouvelle démonstration. Le théorème était démontré depuis 1995. Selon Anthropic, les agents se sont appuyés sur une version simplifiée de la preuve de Wiles due à Darmon, Diamond et Taylor et ont repris des éléments du projet de formalisation de l'Imperial College et du projet flt-regular. Quand on lit qu'une IA a résolu le théorème de Fermat, il ne faut donc pas penser à une nouvelle découverte mathématique, mais à une vérification. Anthropic distingue expressément ce résultat des travaux d'IA sur l'hypothèse de Riemann, où du nouveau aurait été découvert.

Qu'est-ce que Lean ? Un assistant de preuve qui n'omet aucune étape

L'assistant de preuve Lean est un langage de programmation open source qui permet d'écrire des démonstrations mathématiques de manière à ce qu'un ordinateur puisse les vérifier. Le site lean-lang.org décrit Lean comme un langage de programmation et un assistant de preuve doté d'un noyau minimal et digne de confiance, qui garantit l'exactitude. Lean a été conçu par Leonardo de Moura et publié en open source en 2013, comme le rapporte la Simons Foundation. Depuis 2023, la Lean FRO, une organisation à but non lucratif, en assure le développement, soutenue notamment par 5 millions de dollars de la Simons Foundation International.

Le principe se résume simplement. Une démonstration dans Lean est un programme. Le noyau de Lean vérifie pas à pas que chaque conséquence découle des axiomes et de théorèmes déjà vérifiés. Les axiomes sont les hypothèses de base des mathématiques, admises sans preuve. Une étape qui ne découle pas est rejetée, aussi convaincante soit-elle. Là où une preuve manque encore, Lean affiche le marqueur « sorry ». Une démonstration qui en contient est considérée comme incomplète.

C'est précisément ce qui rend Lean si utile pour les modèles d'IA. Les modèles de langage savent formuler de façon convaincante tout en commettant des erreurs. En mathématiques, c'est un problème, car une erreur à l'étape 400 peut invalider tout ce qui suit. Avec un assistant de preuve comme Lean, la question de savoir s'il faut croire le modèle ne se pose plus.

Une relecture humaine fonctionne autrement. Des spécialistes lisent une démonstration, la jugent plausible et se fient à leur expérience. C'est précieux, mais cela prend du temps et laisse place à ce qui passe inaperçu. Dès 2021, un projet collectif a validé dans Lean une démonstration complexe de Peter Scholze, comme le relate la Simons Foundation. La vérification par l'assistant de preuve ne remplace pas la compréhension mathématique, mais elle apporte la certitude de l'exactitude.

Le déroulement de la figure 1 montre la répartition des rôles : le modèle fait des propositions, le noyau de Lean tranche. Peu importe qu'une proposition vienne d'un humain, d'un modèle ou d'un générateur aléatoire, le verdict reste le même.

Mathlib et la question de savoir qui vérifie ce qui a été vérifié

Lean seul ne contient pas encore de mathématiques. Celles-ci se trouvent dans Mathlib, la bibliothèque développée collectivement sur laquelle reposent presque toutes les formalisations. Le site de Lean mentionne plus d'un million de lignes. La page de statistiques de la communauté indiquait lors de la consultation 139 391 définitions, 290 502 théorèmes et 772 contributeurs. Qui démontre quelque chose dans Lean peut s'appuyer sur ces briques vérifiées au lieu de repartir de zéro.

À titre de comparaison, la démonstration de Fermat compte, selon Anthropic, environ 13 millions de lignes et fait donc plus de cinq fois la taille de Mathlib. Cela ressemble à une construction colossale, mais montre aussi combien la vérification formelle coûte pour des théorèmes profonds, même lorsque Mathlib fournit la base. La démonstration dépend de ce qui est déjà formalisé dans Mathlib.

Il faut poser deux questions de vérification distinctes. Premièrement : la démonstration est-elle correcte ? Lean y répond. Anthropic indique que seuls les trois axiomes standard sont utilisés. Deuxièmement : a-t-on réellement démontré le théorème de Fermat et non un énoncé modifié ? Un outil de comparaison (comparator) a été employé ici et a confirmé que l'énoncé formalisé correspond à la formulation de Mathlib. Cette séparation est décisive. Une démonstration sans faille d'un énoncé erroné serait sans valeur.

La démonstration complète est disponible, avec une explication écrite, sur GitHub, selon Anthropic, et peut y être consultée. Seul le modèle utilisé n'est pas public.

Kevin Buzzard, de l'Imperial College de Londres, qui dirige le projet de formalisation depuis 2024, a examiné la démonstration. Selon Anthropic, il constate que le théorème est démontré sans autre hypothèse que les axiomes des mathématiques. Une limite demeure : Lean vérifie l'exactitude, pas la signification. L'outil ne dit pas si un résultat est intéressant, élégant ou important. La Simons Foundation rapporte des appréciations similaires d'Alex Kontorovich.

IA agentique : pourquoi l'essaim a fonctionné

Plusieurs dizaines d'agents ont travaillé en parallèle. Un agent est ici un modèle de langage qui ne se contente pas de répondre, mais utilise de façon autonome des outils, modifie des fichiers et vérifie des résultats intermédiaires. L'infrastructure multi-agents reposait sur Claude Code. Les agents ont défini des notions, démontré des lemmes intermédiaires et les ont utilisés pour des énoncés plus difficiles. L'article Das Zeitalter der KI-Agenten (en allemand) en propose une introduction générale.

Selon Anthropic, la percée n'est pas venue d'un modèle plus puissant, mais d'une meilleure organisation. La plateforme Prove2Me, une plateforme de collaboration ouverte de Tianyi Peng et de ses collègues de l'université Columbia, offrait trois atouts :

• Un graphe orienté acyclique des énoncés de théorèmes servait de repère : chaque énoncé indique de quoi il dépend, et il n'y a pas de cycles.
• Les énoncés et les démonstrations se trouvaient dans des fichiers séparés. Cela accélère la compilation de Lean, car il n'est pas nécessaire de tout revérifier à chaque modification.
• Les théorèmes déjà démontrés pouvaient être retrouvés et réutilisés grâce à des descriptions en langage naturel.

Les tentatives antérieures sans cette structure ont échoué parce que les agents perdaient l'état du projet. Il est instructif que ces tentatives aient tout de même fourni environ 7 pour cent des lignes non triviales de la démonstration finale. La leçon : pour les grandes tâches, la structure l'emporte sur la puissance brute du modèle. Qui déploie de nombreux agents a besoin d'un plan commun, d'un stockage partagé et de responsabilités claires. Les développeurs font la même expérience dans tout projet d'agents un peu important.

La part humaine est restée faible, mais pas nulle. Tianyi Peng a donné de temps à autre des consignes de haut niveau, par exemple prioriser la jacobienne comme schéma ou terminer rapidement le théorème de Mazur. D'après la sortie d'agent citée, le système a signalé le résultat racine comme démontré le 18 août à 02:00:57 UTC.

De l'olympiade aux problèmes d'Erdős : les preuves par IA depuis 2024

L'annonce sur Fermat n'est pas isolée. Depuis 2024, plusieurs résultats montrent que l'IA peut démontrer des théorèmes, et ils diffèrent selon que Lean a été utilisé ou non.

En juillet 2024, AlphaProof avec AlphaGeometry 2 a résolu quatre des six problèmes de l'Olympiade internationale de mathématiques et obtenu 28 points sur 42, niveau argent. Le seuil de l'or était de 29 points. AlphaProof démontre dans Lean et a résolu entre autres le problème le plus difficile du concours. Toutefois, les énoncés avaient d'abord été traduits à la main en langage formel, et le temps de calcul atteignait trois jours par problème. Les participants disposent de deux fois 4 heures 30.

En juillet 2025, Gemini Deep Think a obtenu 35 points sur 42, niveau or, évalué officiellement par les coordinateurs de l'olympiade. Le système a travaillé en langage naturel, dans le temps imparti et sans Lean. C'est un contraste voulu : même sans vérification formelle, l'IA devient performante, mais ses résultats ne sont alors pas vérifiés par machine et doivent être lus par des humains. L'entreprise Harmonic décrit dans une publication sur arXiv son système Aristotle, qui associe une recherche de preuves fondée sur Lean, un raisonnement informel et un solveur de géométrie, et qui atteint, d'après le résumé, un niveau or aux problèmes de 2025.

Début 2026, les problèmes d'Erdős sont entrés dans le champ, une vaste collection de questions ouvertes du mathématicien Paul Erdős. Un exemple est le problème 728, dont la démonstration par Aristotle dans Lean est documentée dans un article sur arXiv. Selon la Simons Foundation, un jeune homme de 23 ans a en outre résolu début 2026 le problème 1196 avec ChatGPT et Lean.

L'appréciation reste prudente. Le wiki de Terence Tao sur les contributions de l'IA aux problèmes d'Erdős se présente expressément comme n'étant pas un benchmark. Il signale un biais de sélection, car les succès sont documentés plus volontiers que les échecs. Il rappelle que l'absence de progrès antérieurs tient souvent à la méconnaissance du problème plutôt qu'à sa difficulté, que l'on retrouve fréquemment après coup de la littérature existante et qu'un problème résolu n'est pas automatiquement un travail publiable. En même temps, le wiki recommande de vérifier formellement les preuves d'IA dans Lean.

Le domaine des preuves par IA en mathématiques va des problèmes de concours aux problèmes marginaux et jusqu'aux grandes formalisations. Le développement est rapide ; il faut vérifier au cas par cas si chaque annonce tient les promesses de son titre. C'est exactement à cela que sert un outil de vérification comme Lean.

Que valent 11 jours ? Une comparaison sans exagération

Les chiffres invitent à de grandes comparaisons. Fermat a formulé le théorème en 1637, Wiles l'a démontré en 1995, soit 358 ans. Le projet de formalisation de l'Imperial College a démarré en 2024, avec un blueprint de 86 pages, et était prévu à l'origine sur plusieurs années. La formalisation par l'IA a duré 11 jours.

Cette comparaison boite pour plusieurs raisons :

• Les 11 jours correspondent à la durée d'exécution d'un essaim d'agents, pas au temps de calcul d'un seul modèle.
• La démonstration était connue. L'IA n'avait pas à trouver une idée nouvelle, mais à traduire dans Lean une structure de preuve existante.
• Il y avait un travail préalable : Mathlib, du matériel du projet de l'Imperial College et de flt-regular, ainsi qu'un blueprint.
• L'effort d'environ six milliards de tokens de sortie d'un modèle interne est considérable. Le coût financier n'est pas indiqué.

Mettre sur le même plan 11 jours de travail de l'IA et des siècles de travail humain sur le problème n'est donc qu'une comparaison rhétorique. Ce qui est exact : un travail qu'un projet collectif avait planifié sur des années a été pour l'essentiel achevé en quelques jours.

Une expérience annexe ramène à la vie quotidienne. Selon Anthropic, trois abonnements Claude Max personnels ont formalisé en trois jours le théorème des trois nombres premiers de Vinogradov. Les auteurs jugent possible une formalisation collective avec des abonnements grand public, si l'infrastructure est adaptée. C'est une appréciation des auteurs, non un résultat établi de façon indépendante.

Limites et points ouverts : ce que l'annonce ne montre pas

Anthropic mentionne elle-même des limites. La démonstration est vraisemblablement nettement plus longue que nécessaire, car Mathlib est plus compacte et mieux vérifiée. Elle dépend de ce qui est déjà formalisé dans Mathlib. Le modèle utilisé est un modèle de recherche interne et non public, si bien que le résultat ne peut pas être reproduit de l'extérieur avec les mêmes moyens.

D'autres points restent ouverts :

• Aucune mathématique nouvelle n'a été produite. La formalisation accroît la certitude, pas le savoir.
• Une démonstration dans Lean n'est pas automatiquement compréhensible. Personne ne lit 13 millions de lignes du début à la fin.
• Lean ne dit rien de l'importance d'un théorème, seulement de son exactitude.
• Le degré d'indépendance de la vérification, au-delà de l'appréciation de Buzzard, ne ressort pas de l'annonce.

Pour d'autres annonces isolées, par exemple sur des avancées concernant l'hypothèse de Riemann ou sur des agents d'autoformalisation de certaines entreprises, cette recherche ne dispose d'aucune source primaire vérifiable. Ces annonces restent donc ici sans chiffres. Les appréciations de spécialistes ne sont reprises que lorsque la déclaration originale est disponible.

Ce que l'approche de Lean signifie au-delà des mathématiques

Le schéma qui sous-tend le projet Fermat est généralisable : essais libres d'un côté, validation stricte de l'autre. Il convient partout où un résultat est vérifiable par machine. Le site de Lean cite comme applications hors des mathématiques la vérification d'ArkLib, une bibliothèque consacrée aux SNARK (preuves cryptographiques compactes), et de Cedar, le langage d'autorisation d'AWS. En développement logiciel, le principe est connu : un compilateur et une exécution de tests valident eux aussi ce qu'un humain ou une IA a écrit.

Il en découle une règle empirique pour l'usage des productions d'IA. Plus un résultat se prête à une vérification automatique, plus un modèle peut travailler librement. Pour les textes, les évaluations et les recommandations, cette validation stricte fait le plus souvent défaut. Là, l'humain reste le vérificateur.

La même logique vaut pour la sécurité et la protection des données : des propriétés démontrables comptent plus que de simples affirmations. Qu'un site charge des traceurs ou définisse des en-têtes de sécurité, par exemple, peut se mesurer automatiquement. Le contrôle de site web de Dr. DSGVO en offre la possibilité, et les propriétés techniques de sécurité peuvent être vérifiées avec les Security-Checks. Ce ne sont pas des preuves formelles au sens de Lean, mais elles suivent la même idée : mesurer plutôt que croire.

Les essais de Dr. DSGVO

Avec l'aide de l'IA, la démonstration mathématique a (vraisemblablement) été établie et formalisée : des hexagones magiques existent, selon une certaine règle de construction, pour tout n quelconque (n = longueur d'une arête de l'hexagone, en alvéoles).

Le temps de calcul total de l'IA a été de presque 9 heures. Pendant environ 99,9 % de ce temps, le système a travaillé de façon autonome sans nécessiter d'entrées. Les fichiers de la démonstration représentaient 173 Mo ! La formalisation avec Lean et ses bibliothèques a consommé près de 8 Go d'espace disque – en étapes intermédiaires ! La démonstration entière s'est étalée sur 5 jours. Elle a été interrompue en raison de limites d'utilisation ou similaires.

La démonstration sera prochainement publiée ici. Reste à savoir si elle est juste : c'est à des personnes compétentes, qui comprennent mieux les mathématiques que l'auteur, qui a utilisé l'IA, d'en juger 😉

Conclusion : la révolution, c'est la vérifiabilité

L'IA n'a pas démontré à nouveau le dernier théorème de Fermat, mais a formalisé intégralement dans Lean la démonstration de Wiles, en 11 jours selon Anthropic, avec plusieurs dizaines d'agents en parallèle. Le succès repose sur deux choses : une organisation qui garde l'état du projet visible, et l'assistant de preuve Lean, qui n'accepte que ce qui découle.

L'évolution depuis 2024 montre que l'IA produit de plus en plus de démonstrations mathématiques. La part de nouveauté et la part de matériel connu doivent être évaluées au cas par cas, le wiki de Tao y invite aussi. Là où Lean est en jeu, l'exactitude reste vérifiable. C'est le véritable progrès : non plus des affirmations, mais une certitude vérifiée par machine.