Numérique

La société Axiom Math a annoncé le 17 août 2026 que son système AxiomProver avait produit une preuve vérifiée par machine, rédigée en Lean 4, du résultat le plus solide connu à ce jour sur les écarts entre nombres premiers : il existe une infinité de paires de nombres premiers dont la différence ne dépasse pas 246. Ce travail, attribué à 41 contributeurs issus des mathématiques et de l'ingénierie, a d'abord été signalé par IEEE Spectrum.

Pour comprendre l'enjeu, il faut remonter à la conjecture des jumeaux premiers, formulée au XIXe siècle par Alphonse de Polignac, qui postule l'existence d'une infinité de paires de premiers séparés exactement de deux — conjecture toujours non démontrée. La première percée décisive est venue en 2013, quand Yitang Zhang établit qu'une infinité de paires de premiers sont distantes d'au plus 70 millions. Peu après, James Maynard, grâce à une méthode de crible raffinée, ramena cette borne à 600 — contribution qui contribua à lui valoir la Médaille Fields en 2022. La collaboration Polymath8b, à laquelle participaient Maynard et Terence Tao, abaissa ensuite la borne à 246, valeur qui constitue aujourd'hui, selon Ken Ono, mathématicien fondateur d'Axiom Math, « la limite des connaissances humaines sur les nombres premiers ».

La formalisation réalisée par Axiom Math synthétise ces deux étapes : l'article de Maynard de 2013 et la partie de Polymath8b qui a conduit à 246. Le processus s'est déroulé en trois temps : rédaction d'un plan structuré listant chaque définition, lemme et théorème avec ses dépendances ; génération automatique des preuves Lean 4 par AxiomProver, un système multi-agents s'appuyant sur Mathlib et sur le projet PrimeNumberTheoremAnd dirigé par Alex Kontorovich et Tao ; puis révision humaine du code produit. Les résultats sont rassemblés dans une bibliothèque publique baptisée PrimeGapsLib, qui inclut également la borne de 600 de Maynard et un défi de vérification indépendant permettant à quiconque de contrôler que les preuves correspondent bien aux énoncés annoncés.

La vérification formelle ne constitue pas une garantie absolue — la traduction fidèle des énoncés et la fiabilité du noyau vérificateur restent des prérequis — mais elle élimine le risque d'erreur humaine dans la relecture. Contrairement aux benchmarks de compétition sur lesquels les IA sont habituellement évaluées, il s'agit ici de formaliser une preuve de recherche parmi les plus exigeantes de la théorie des nombres moderne. À titre de comparaison, Math, Inc. avait conduit en début d'année une formalisation des travaux de Maryna Viazovska sur l'empilement de sphères ; l'un des artisans de cet effort, Sidharth Hariharan, est depuis contributeur chez Axiom Math sur le projet 246 et estime que PrimeGapsLib constitue une réalisation plus complète, car conçue comme une infrastructure réutilisable et non comme une vérification ponctuelle. Ken Ono voit dans cet outil un terrain d'entraînement pour une ambition plus large : la vérification formelle du code informatique qui régit déjà des systèmes critiques de finance, d'infrastructure et de sécurité.

Les modèles de langage peinent traditionnellement en mathématiques, commettant des erreurs sur des calculs élémentaires. Pour remédier à ce problème, Apple développe un petit moteur de calcul local intégré à Siri, disponible à partir de la bêta 5 de macOS 27, qui prend le relais lors de questions mathématiques.

Ce MathComputeTool est capable de traiter des requêtes en langage naturel : arithmétique basique (y compris avec plusieurs opérations), conversions de fractions, calculs de surfaces, racines carrées et puissances. Contrairement aux calculatrices classiques de macOS, il accepte les formulations conversationnelles et fonctionne hors ligne, offrant aux utilisateurs une alternative plus fiable que l'actuel Siri pour des questions mathématiques.

La question des capacités réelles des grands modèles de langage (LLM) en mathématiques fait l'objet d'un débat animé dans la communauté scientifique, alimenté par plusieurs travaux et prises de position récentes. D'un côté, une étude présentée à la conférence ICML 2026 par Tom Zahavy, chercheur chez Google DeepMind, intitulée « LLMs can't jump », propose un cadre analytique pour caractériser les limites de ces systèmes. L'auteur y distingue trois formes de raisonnement — l'induction, la déduction et l'abduction — pour mieux cerner ce que les LLM font ou ne font pas lorsqu'ils sont confrontés à des problèmes nouveaux.

De leur côté, deux mathématiciens de premier plan, Timothy Gowers, médaillé Fields, et Peter Sarnak, portent un jugement nuancé sur ces outils. Ils reconnaissent que les LLM sont performants pour assembler et combiner des techniques mathématiques déjà connues, mais ils estiment que ces systèmes sont dépourvus de l'intuition nécessaire à la production d'idées véritablement originales. Cette distinction entre capacité computationnelle et créativité constitue le coeur de leur analyse.

Pourtant, les mêmes sources soulignent des avancées concrètes qui compliquent ce tableau. Un modèle d'OpenAI aurait ainsi résolu une conjecture de Paul Erdos portant sur la géométrie à distance unitaire, restée ouverte depuis 1946, en mobilisant des outils issus de la théorie des nombres algébriques — une approche jugée inédite par les experts. Ce résultat, validé par neuf mathématiciens et supervisé par trois chercheurs d'OpenAI, a conduit Gowers lui-même à qualifier cette avancée de jalon important pour l'IA en mathématiques, tout en notant qu'il devient de plus en plus difficile pour les humains de rivaliser sur certains terrains.

Par ailleurs, les progrès des LLM semblent plus marqués dans les domaines où les résultats sont vérifiables, comme la programmation ou les preuves formelles, notamment grâce aux techniques d'apprentissage par renforcement. En revanche, des travaux récents montrent que les hallucinations de ces modèles — leurs réponses fausses mais assurées — ne résultent pas d'un simple manque de données, mais sont ancrées dans leur architecture même : les trajectoires internes des modèles peuvent diverger et s'éloigner activement des bonnes réponses.

Ce tableau d'ensemble dessine une réalité contrastée : des LLM capables de performances surprenantes sur des problèmes précis et vérifiables, mais dont la créativité mathématique au sens fort — celle qui consiste à forger des concepts radicalement nouveaux — reste, pour l'heure, une limite reconnue par les spécialistes eux-mêmes.

Depuis l'automne 2025, l'intelligence artificielle multiplie les avancées spectaculaires dans le domaine des mathématiques, au point de résoudre des problèmes restés ouverts depuis des décennies, voire près d'un siècle.

L'une des percées les plus remarquables concerne la conjecture dite des « distances unitaires », formulée en 1946 par le mathématicien hongrois Paul Erdos (1913-1996). Ce problème, classé parmi les dix plus difficiles de la liste des 1 217 énigmes laissées par Erdos, posait la question du nombre de paires de points séparés par une distance exactement égale à 1 parmi un ensemble de n points dans le plan. La conjecture était généralement tenue pour vraie par la communauté mathématique, qui cherchait à la démontrer. Le 20 mai 2026, OpenAI a annoncé qu'elle avait été réfutée par ChatGPT dans sa version 5.2, sortie en décembre 2025. Fait notable : la solution n'a pas été produite par des chercheurs ou des ingénieurs d'OpenAI, mais par de simples amateurs utilisant leur abonnement personnel. La démonstration, publiée formellement, a été validée par des mathématiciens de renom. Ce qui déconcerte les spécialistes tient moins au résultat qu'à la méthode : l'IA a mobilisé des champs mathématiques que personne n'avait envisagé d'appliquer à ce problème. Le mathématicien Arul Shankar la qualifie de preuve « très humaine, quoique d'une ingéniosité extrême ».

Cette réussite s'inscrit dans un contexte plus large d'effervescence. Le 19 juillet, Levent Alpöge, mathématicien chez Anthropic, a annoncé que Claude Fable 5 avait réfuté la conjecture jacobienne, énoncée en 1939 par le mathématicien allemand Ott-Heinrich Keller et jamais démontrée depuis. Le 10 août, Anthropic a révélé qu'une version non publiée de Claude avait progressé sur un problème lié à la célèbre hypothèse de Riemann, formulée en 1859 et dotée d'une récompense d'un million de dollars : l'IA a coordonné de manière autonome une soixantaine de sous-agents, exécuté 2 400 commandes et procédé à des relectures croisées, tandis que l'unique contribution humaine consistait, selon Anthropic, à envoyer des messages d'encouragement. Le 1er août, OpenAI publiait de son côté un manuscrit de 249 pages annonçant que son futur modèle Astra aurait résolu dix problèmes ouverts en mathématiques et en informatique théorique.

Ces annonces suscitent cependant des réserves dans la communauté scientifique. Début juin, la déclaration de Leiden, signée par quelque 3 500 chercheurs dont le médaillé Fields Peter Scholze, a mis en garde contre des résultats diffusés via des communiqués de presse avant toute validation par les pairs, risquant de « surestimer l'importance des outils automatisés ». La prudence est d'autant plus de mise qu'à l'automne 2025, des problèmes d'Erdos présentés comme résolus par ChatGPT s'étaient révélés simplement retrouvés dans la littérature existante. Pour François Charles, directeur du département de mathématiques de l'École normale supérieure, ces outils représentent néanmoins « une vraie révolution scientifique » qui, loin de condamner les mathématiciens, ouvre un nouveau champ des possibles.

OpenAI a publié le 1er août 2026 un manuscrit de 249 pages documentant la résolution de dix problèmes mathématiques majeurs par son système Astra : un groupe non sofique explicite (27 ans après sa formulation par Gromov), la réfutation de la conjecture de rigidité de Connes, et huit autres résultats inédits en géométrie haute dimension, complexité quantique, cryptographie sur réseaux et combinatoire extrémale. Les preuves sont formalisées en Lean 4 et publiées sous licence Apache 2.0.

Le coût d'inférence estimé à 2 000 dollars soulève des questions sur l'investissement réel en entraînement et infrastructure, tandis que la mise en forme reste artisanale. Noam Brown (OpenAI) a précisé qu'Astra n'avait pas attaqué les problèmes du prix du millénaire, maintenant une distinction nette entre ces résultats et les sept énigmes majeures restantes.

Astra demeure entièrement inaccessible au public. OpenAI a accordé un accès gratuit à ses modèles frontière pour 100 000 chercheurs académiques jusqu'en 2027 et soumis le système à un examen gouvernemental avant déploiement commercial. La crédibilité de l'annonce repose désormais sur la vérification indépendante par la communauté mathématique des 249 pages et preuves formelles.

Le 1er août 2026, OpenAI a publié un rapport faisant état d'une avancée spectaculaire : une version interne d'Astra, sa prochaine grande famille de modèles de langage, aurait résolu dix problèmes mathématiques ouverts dans des domaines particulièrement ardus. Parmi eux figurent la géométrie en grande dimension, la théorie des codes, la complexité quantique, la cryptographie sur réseaux et la combinatoire extrémale — des sujets sur lesquels la communauté scientifique butait depuis au moins une décennie, parfois bien davantage. Concrètement, le modèle aurait entre autres établi l'existence de groupes dits non sofiques, réfuté la conjecture de rigidité de Connes, prouvé un théorème quantique de répétition parallèle et amélioré pour la première fois depuis 1978 une borne sur la densité d'empilement de sphères. L'ensemble de ces arguments, entièrement générés par l'IA selon OpenAI, a ensuite été formalisé dans le langage de vérification Lean, qui garantit l'exactitude logique des preuves de manière automatique. Le coût de calcul annoncé est d'environ 2 000 dollars par problème aux tarifs de l'API, ce qui tranche radicalement avec les années, parfois les décennies, qu'auraient nécessitées des équipes humaines. Noam Brown, chercheur chez OpenAI, parle d'un « pas majeur pour le raisonnement scientifique », tout en reconnaissant qu'aucun des sept Problèmes du Prix du Millénaire — dotés chacun d'un million de dollars — n'a pu être résolu. Du côté des mathématiciens, les réactions mêlent émerveillement et inquiétude. Timothy Gowers, médaillé Fields, a rapporté qu'un outil d'OpenAI avait résolu dès la première tentative deux problèmes sur lesquels il travaillait depuis longtemps. Le mathématicien Jay Cummings a confié l'étrangeté de voir une machine venir à bout d'un sujet auquel il avait consacré des années. Thomas Bloom, de l'université de Manchester, juge les résultats d'Astra plus significatifs encore que la récente réfutation de la conjecture de distance unitaire, tout en rejetant l'idée d'un remplacement pur et simple des chercheurs. La question de l'attribution de la paternité scientifique surgit également : OpenAI estime qu'attribuer ces preuves à des humains serait inexact, puisque les arguments mathématiques ont été produits de façon autonome par le modèle. Au-delà de la prouesse technique, une autre difficulté émerge, signalée notamment par le mathématicien Terence Tao : l'IA génère désormais un flux de résultats si abondant que la communauté scientifique peine à les vérifier et à les assimiler. Ce déséquilibre entre la vitesse de production et la capacité humaine d'évaluation constituerait un problème inédit pour la discipline. Jacob Tsimerman, futur lauréat de la médaille Fields 2026, a récemment quitté l'université de Toronto pour rejoindre OpenAI, signe du bouleversement en cours. Il estime que si la tendance se confirme, il faudra très prochainement « repenser le fonctionnement de toute la discipline ».

Un neurochirurgien pékinois aux antécédents atypiques vient peut-être d'écrire une page importante de l'histoire des mathématiques. Jin Shanmu, chercheur postdoctoral au Peking Union Medical College Hospital, a grandi géologue avant de bifurquer vers la médecine, puis vers la recherche sur les ultrasons transcrâniens. Sa formation en mathématiques se limitait aux cours de premier cycle, le reste étant autodidacte. C'est en travaillant sur ces ultrasons cérébraux qu'il a croisé la conjecture de Crouzeix, un problème resté ouvert depuis 2004.

Formulée par le mathématicien français Michel Crouzeix, cette conjecture relève de l'algèbre linéaire numérique : elle affirme que la norme de l'application d'une fonction à une matrice ne dépasse jamais le double du maximum de cette fonction sur le domaine numérique de la matrice. Concrètement, cela touche à des questions fondamentales d'analyse matricielle, utilisée en physique et en informatique. Pendant vingt ans, les meilleurs spécialistes du domaine n'étaient parvenus ni à prouver ni à réfuter cette propriété.

Pour tenter de percer ce mystère, Jin Shanmu a eu recours à GPT-5.6-Sol, la version avancée du modèle d'OpenAI, qu'il a laissé travailler de manière autonome pendant seize heures sur la plateforme ChatGPT Work. Le résultat est une démonstration complète, que Jin a rédigée sous forme d'article et déposée en ligne le 27 juillet 2025.

Trois jours plus tard, le mathématicien Alex Townsend, de l'université Cornell, qui consultait régulièrement depuis plus d'un an les modèles GPT pour attaquer cette même conjecture, a été informé par l'IA de l'existence de cet article. Avec Anne Greenbaum, professeure à l'université de Washington, et Michel Crouzeix lui-même, il a examiné le manuscrit. Tous trois ont jugé la démonstration correcte. Townsend et Greenbaum ont publié un compte rendu de ces échanges, soulignant les capacités "remarquablement impressionnantes" de GPT-5.6, d'autant plus frappantes eu égard à l'absence de formation spécialisée de Jin. La preuve n'a toutefois pas encore fait l'objet d'une évaluation formelle par les pairs, étape indispensable avant toute validation définitive.

Cet épisode s'inscrit dans un mouvement plus large. En mai 2025, OpenAI avait annoncé qu'un modèle interne de raisonnement avait autonomement progressé sur un problème posé par le mathématicien hongrois Paul Erdos en 1946. La société a depuis publié une liste de dix autres problèmes sur lesquels son futur modèle Astra aurait réalisé des avancées significatives. De son côté, Anthropic a indiqué que son modèle Claude, sans parvenir à démontrer l'hypothèse de Riemann, avait néanmoins produit des résultats inattendus sur une question connexe. L'intelligence artificielle semble désormais capable non seulement de suivre des pistes humaines, mais d'en proposer de nouvelles.

Anthropic a annoncé que son modèle d'IA Claude Mythos Preview a identifié des vulnérabilités mathématiques fondamentales dans deux algorithmes cryptographiques majeurs. La première cible HAWK, un système de signature numérique en lice pour standardisation par le NIST américain : en 60 heures, l'IA a exploité une symétrie mathématique non détectée en deux ans d'examen expert, réduisant la complexité effective de HAWK-256 de 2^64 à 2^38, ce qui élimine les garanties qui rendaient ce schéma attractif pour la cryptographie post-quantique.

La seconde découverte porte sur AES, le standard de chiffrement mondial. Claude a développé « Möbius Bridge », une technique qui améliore une méthode d'attaque existante contre AES-7 rounds (version affaiblie étudiée académiquement), rendant l'attaque théorique 200 à 800 fois plus rapide en éliminant une étape de devinette massive. Ces résultats n'ont pas d'impact immédiat sur les utilisateurs, mais soulèvent des questions fondamentales : chaque découverte a coûté environ 100 000 dollars, et le goulot d'étranglement est devenu humain — un mois de travail a été nécessaire pour valider la méthode contre AES. Anthropic s'interroge sur la conduite à tenir si une IA découvrait une vulnérabilité ayant un impact réel et immédiat.

Un modèle de recherche inédit d'Anthropic vient de réaliser ce que les mathématiciens n'avaient pas réussi à accomplir en 37 ans : faire progresser significativement la conjecture de Riemann, l'un des grands problèmes non résolus des mathématiques depuis 1859. Ce problème porte sur la distribution des nombres premiers et est assorti d'une récompense d'un million de dollars par l'Institut Clay. Plus précisément, la conjecture prédit que les zéros d'une certaine fonction mathématique — la fonction zêta de Riemann — s'alignent tous sur une droite verticale particulière appelée droite critique. Si personne n'a encore pu le prouver ou le réfuter dans sa globalité, les mathématiciens cherchaient au moins à établir quelle proportion minimale de ces zéros respecte cette règle. Depuis 1989, ce seuil était bloqué à 41,6 %. En un jour et demi seulement, le modèle d'Anthropic l'a porté à 67,2 %, soit le bond le plus important jamais accompli depuis l'énoncé de la conjecture.

La démarche est aussi remarquable que le résultat. Un employé d'Anthropic sans formation mathématique poussée a simplement demandé au modèle de « s'attaquer sérieusement » au problème, puis l'a laissé travailler de façon autonome. Le modèle a d'abord testé 650 pistes infructueuses lors d'une première session. Lors de la seconde, il a coordonné une soixantaine de sous-agents, exécuté des milliers de commandes et scripts, téléchargé 54 articles scientifiques pour s'assurer de l'originalité de sa découverte, avant de formaliser un résultat en 31 millions de tokens de sortie. Sa contribution essentielle a consisté à combiner deux lignes de recherche existantes — des travaux récents de Baluyot, Goldston, Suriajaya et Turnage-Butterbaugh, et un article de Bombieri datant de 2000 — que les spécialistes, cantonnés chacun dans leur domaine, n'avaient pas encore reliées entre elles.

La rigueur du résultat a été soigneusement vérifiée : deux mathématiciens d'Anthropic, Levent Alpöge et Ralph Furman, ont examiné la démonstration en détail ; une preuve formelle a été rédigée dans le langage de vérification automatique Lean et validée avec succès ; et deux experts extérieurs de premier plan, Brian Conrey et Dan Goldston — dont les propres travaux ont servi de fondation au résultat — ont accepté de relire le papier. Des limites importantes sont toutefois reconnues : la preuve n'a pas encore été soumise à une revue par les pairs classique, et le modèle utilisé n'est pas encore disponible publiquement, ce qui rend la reproduction exacte de la démarche impossible pour l'instant.

Cette avancée s'inscrit dans un contexte plus large d'accélération des capacités mathématiques des intelligences artificielles. Quelques jours plus tôt, un autre modèle d'Anthropic avait, selon plusieurs sources, produit un contre-exemple réfutant la conjecture jacobienne, ouverte depuis 1939. OpenAI aurait également annoncé des résultats sur plusieurs problèmes non résolus. Ces succès successifs relancent le débat dans la communauté scientifique sur le rôle de l'IA en recherche mathématique, entre enthousiasme face à ces capacités nouvelles de synthèse et interrogations sur la notion d'auteur et de responsabilité dans la production de preuves.