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

Axiom Math a produit une preuve formelle vérifiée par machine du résultat connu le plus fort sur les écarts entre nombres premiers : il existe une infinité de paires de nombres premiers distants d'au plus 246. Ce théorème, formalisé en Lean 4 et publié le 17 août 2026, représente l'aboutissement d'une progression historique : Yitang Zhang avait d'abord prouvé en 2013 une borne de 70 millions, James Maynard l'a réduite à 600 (travail récompensé par la Médaille Fields en 2022), et la collaboration Polymath8b incluant Terence Tao l'a affinée à 246.

La formalisation suit une approche novatrice en trois étapes : rédaction d'un plan détaillé du théorème et ses dépendances, génération par AxiomProver (système multi-agents d'Axiom Math) de preuves Lean 4 vérifiables, puis révision et organisation en bibliothèque publique PrimeGapsLib. Contrairement aux formalisations ponctuelles, cette bibliothèque est conçue pour la réutilisation et l'extension, incluant également la borne de 600 et un défi de vérification autonome permettant à quiconque de valider indépendamment les résultats.

Ce résultat se distingue des affirmations récentes d'IA en mathématiques de recherche : il ne revendique pas un nouveau théorème mais démontre qu'un système peut formaliser vérifiablement l'une des preuves les plus techniquement complexes de la théorie des nombres contemporaine, marquant un franchissement de l'écart entre succès en compétitions mathématiques et rigueur formelle au niveau de la recherche.