L’IA d’Axiom Math vérifie le théorème des écarts de 246 nombres premiers dans Lean

Axiom Math affirme que son système AxiomProver a produit une preuve Lean 4 vérifiée par machine du résultat le plus fort connu sur les écarts entre nombres premiers: le théorème selon lequel un nombre infini de paires de nombres premiers diffèrent de au plus 246. L’entreprise a publié le résultat le 17 août 2026 sous forme de plan de formalisation interactif attribué à 41 contributeurs nommés en mathématiques, ingénierie et en tant que chercheurs principaux, IEEE Spectrum ayant d’abord rapporté cette étape.

La borne de 246 représente aujourd’hui la limite des connaissances humaines dans la longue lutte contre la conjecture des jumeaux premiers, hypothèse du XIXᵉ siècle selon laquelle des nombres premiers séparés exactement de deux réapparaissent indéfiniment. La page projet d’Axiom Math décrit le travail comme une formalisation unifiée de l’article de James Maynard de 2013 « Small gaps between primes » ainsi que de la partie du suivi de la collaboration Polymath8b qui a resserré la borne de Maynard de 600 à 246. Les preuves vérifiées par machine sont organisées dans une bibliothèque publique Lean, PrimeGapsLib, le théorème de 246 étant son résultat phare.

« Ce théorème représente actuellement la limite des connaissances humaines sur les nombres premiers », a déclaré Ken Ono, mathématicien fondateur d’Axiom Math.

La vérification formelle consiste à traduire une preuve dans un langage qu’un petit programme de confiance appelé noyau peut vérifier ligne par ligne. Le résultat n’est pas une garantie absolue — l’énoncé lui‑même doit être correctement traduit, et le vérificateur doit être fiable — mais cela élimine la faillibilité du relecteur humain de la chaîne. Jusqu’à présent, les systèmes d’IA qui concourent aux référentiels de mathématiques ont surtout été évalués sur des problèmes de compétition avec des preuves courtes et autonomes ; l’écart entre ces résultats et la formalisation au niveau de la recherche était important, un schéma visible dans des systèmes antérieurs qui excellaient en géométrie olympique tout en laissant les mathématiques de recherche largement intouchées.

De 70 millions à 246

La conjecture elle‑même, formulée précisément par Alphonse de Polignac au XIXᵉ siècle, reste non démontrée. La première borne finie de quelque nature que ce soit est apparue en 2013, lorsque Yitang Zhang a prouvé que un nombre infini de paires de nombres premiers se trouvent à moins de 70 millions les unes des autres. Quelques mois plus tard, Maynard a introduit une méthode de crible raffinée et a réduit la borne à 600 — travail qui a contribué à sa Médaille Fields en 2022 — et la collaboration Polymath8b, qui incluait Maynard et Terence Tao, l’a fait passer à 246. Le plan d’Axiom Math expose cette progression comme le projet qu’il a cherché à formaliser.

La formalisation suit un pipeline que l’entreprise décrit en trois étapes. Les chercheurs ont d’abord rédigé la preuve sous forme de plan — chaque définition, lemme et théorème recevant une étiquette, une énoncé précis et une liste des résultats dont il dépend — produisant un graphe de dépendances qui ordonnait le travail. AxiomProver, le système multi‑agents de l’entreprise pour la recherche mathématique via la preuve formelle, a ensuite généré des preuves Lean 4 vérifiables par machine, construites sur Mathlib, la bibliothèque communautaire de mathématiques, et sur PrimeNumberTheoremAnd, le projet de formalisation existant dirigé par Alex Kontorovich et Tao. L’équipe d’Axiom a ensuite revu le code généré et l’a organisé dans PrimeGapsLib.

Les principaux résultats annoncés de la bibliothèque vont légèrement au‑delà du théorème principal. En plus de la borne de 246, elle formalise la borne de 600 de Maynard, et elle inclut un défi de vérification autonome — construit uniquement sur Mathlib, avec l’emplacement de la preuve laissé vide — qui permet à quiconque disposant de l’outil de comparaison Lean de confirmer indépendamment que les preuves de la bibliothèque correspondent aux théorèmes annoncés. L’entreprise avertit que la vérification complète peut prendre des heures ; une version réduite couvrant les deux autres résultats s’exécute en quelques minutes.

Où cela se situe parmi les revendications de formalisation IA

Le résultat apparaît dans une année où les affirmations concernant les systèmes d’IA réalisant des mathématiques de niveau recherche se multiplient, la plupart étant ancrées à des scores de compétition ou à des preuves courtes. Axiom Math a été l’un des revendicateurs les plus agressifs: AxiomProver est crédité d’avoir résolu des problèmes auparavant ouverts, y compris des travaux que l’entreprise a publiés dans des revues à comité de lecture, et les systèmes d’IA ont maintenant résolu plusieurs problèmes d’Erdős de longue date. La formalisation de 246 constitue un type de résultat différent — ce n’est pas un nouveau théorème, mais une reconstruction vérifiée par machine d’une des preuves les plus techniquement exigeantes de la théorie des nombres moderne.

La comparaison la plus proche remonte au début de l’année, lorsque Math, Inc. a utilisé son agent Gauss pour achever la preuve formelle des résultats d’empaquetage de sphères de Maryna Viazovska, lauréate de la Médaille Fields, dans les dimensions 8 et 24. Sidharth Hariharan, doctorant à Carnegie Mellon qui a dirigé l’effort humain de planification de cette formalisation et qui est maintenant stagiaire chez Axiom Math ainsi que contributeur mathématique nommé sur le projet 246, soutient que le nouveau résultat constitue l’accomplissement le plus complet. Son raisonnement, tel qu’il l’a décrit, est qu’Axiom a été conçu pour la réutilisation: plutôt qu’une formalisation ponctuelle d’une preuve unique, PrimeGapsLib est une bibliothèque maintenue de résultats d’écarts de nombres premiers destinée à soutenir les futurs travaux et recherches de formalisation.

Cette distinction est importante pour la manière dont le résultat doit être interprété. Une vérification ponctuelle montre qu’un système peut résister à un seul proof difficile. Une bibliothèque montre quelque chose de plus proche d’une infrastructure — une machinerie formelle réutilisable sur laquelle d’autres résultats peuvent s’appuyer — ce qui correspond à la direction que les systèmes de preuve formelle ont pris en passant de la résolution d’exercices à la vérification de mathématiques réelles. La revendication de capacité ici repose sur des artefacts publics et réexécutables plutôt que sur un score de référence: le plan, le code Lean, et un défi de comparaison conçu pour que des chercheurs extérieurs puissent vérifier les preuves eux‑mêmes.

Ono présente les mathématiques comme un banc d’essai pour une ambition plus vaste. Si les propriétés d’un logiciel — que le programme se termine, que sa sortie est correcte pour chaque entrée — peuvent être exprimées sous forme d’énoncés mathématiques précis, alors les systèmes dérivés d’AxiomProver pourraient les prouver formellement, soutient-il, ouvrant la voie à la vérification du code généré par IA qui commence à être utilisé dans les systèmes d’infrastructure, financiers et de sécurité.

« Le monde est sur le point de fonctionner avec du code informatique que personne n’a lu », a déclaré Ono. « L’IA est là et nous ne pouvons plus détourner le regard — la formalisation des preuves est un banc d’essai pour résoudre ce que je pense être le défi le plus important que nous devrons affronter avec l’IA. »

Pour l’instant, le livrable est plus restreint et vérifiable: un plan à 41 auteurs, une bibliothèque publique Lean, et une preuve vérifiée par machine que les nombres premiers situés à moins de 246 les uns des autres ne s’épuisent jamais — le voisin le plus proche vérifié de la conjecture des jumeaux premiers, et la partie la plus profonde de mathématiques de recherche qu’un système d’IA ait jamais vérifiée de bout en bout.