En mai, une question sur des points dans un plan a produit une réponse inattendue. En septembre, des laboratoires d’IA publiaient des arguments sur les singularités des fluides, accompagnés de fichiers permettant aux ordinateurs de vérifier les preuves. Entre ces annonces sont apparus de nouveaux contre-exemples, des bornes améliorées et une formalisation du dernier théorème de Fermat.
Les progrès de l’IA en mathématiques méritent mieux qu’un décompte continu des conjectures réfutées. Ces résultats répondent à des questions différentes, s’appuient sur des éléments de preuve différents et laissent des travaux distincts inachevés. Un contre-exemple peut renverser une croyance sans fournir la meilleure réponse possible. Une meilleure borne peut être importante alors même que la célèbre conjecture voisine reste ouverte. Une preuve vérifiée par ordinateur peut établir un énoncé sans expliquer pourquoi ses idées seront utiles ailleurs.
Nous examinons ici les principaux développements qui relient l’annonce d’OpenAI du 20 mai sur les distances unitaires à l’affirmation de septembre sur Navier-Stokes, en tenant compte des informations disponibles au 22 septembre 2026. Nous incluons les annonces intermédiaires et les travaux qui en ont découlé. Il s’agit d’une carte de cette séquence, et non d’un inventaire exhaustif de chaque article de mathématiques assistées par l’IA. Nous avons lu les annonces citées, les énoncés pertinents des théorèmes, les introductions des recherches et la documentation de vérification. Nous n’avons ni évalué ces preuves de manière indépendante ni reconstruit leurs formalisations.
Nous estimons que les éléments les plus convaincants du progrès comportent deux volets : les machines produisent des arguments mathématiques qui méritent un examen sérieux, et les chercheurs en tirent déjà de nouveaux résultats dans certains cas. Pour que ce progrès se poursuive, il faudra consacrer des ressources à la vérification, à l’explication et au prolongement de ces travaux.
Mai : un contre-exemple ouvre une nouvelle voie en géométrie
Le problème des distances unitaires est facile à visualiser. Placez un ensemble de points sur une surface plane et comptez les paires séparées exactement d’une unité. À mesure que vous ajoutez des points, combien de telles paires peut-on obtenir au maximum ?
Dans son annonce du 20 mai, OpenAI attribue une nouvelle construction à un modèle interne de raisonnement général, évalué sur un ensemble de problèmes d’Erdős. L’entreprise a aussi publié un article compagnon distinct, rédigé par des mathématiciens externes qui ont examiné l’argument. Ce second document compte : les lecteurs peuvent y voir ce que ces mathématiciens ont compris et reconstruit, au-delà du récit du laboratoire sur son modèle. L’annonce d’OpenAI.
Le manuscrit initial construit une infinité d’ensembles de points contenant au moins n^(1+δ) paires à distance unitaire, pour un δ positif fixé. Autrement dit, l’amélioration de l’exposant se maintient à mesure que les exemples grandissent. Cela contredit la conjecture d’une croissance presque linéaire. Le résultat ne détermine pas le nombre maximal exact de distances unitaires pour chaque nombre de points, et la recherche de bornes optimales se poursuit. Le manuscrit sur les distances unitaires.
La surprise venait de l’origine de la construction. L’article compagnon relie le résultat géométrique à une théorie sophistiquée des nombres algébriques et nomme des ingrédients mathématiques antérieurs. Ses auteurs proposent une reconstruction simplifiée et quelque peu généralisée. C’est un exemple utile du travail humain qui suit une découverte de l’IA : identifier le mécanisme, rendre visibles ses dépendances et transformer un argument en quelque chose que d’autres chercheurs peuvent exploiter. L’article compagnon des mathématiciens.
Un lecteur qui cherche la portée du résultat de mai devrait donc suivre les articles publiés ensuite d’aussi près que l’annonce initiale. Une nouvelle technique gagne en crédibilité d’un autre ordre lorsque des chercheurs l’utilisent pour poser puis résoudre d’autres questions.
De mai à juillet : les idées commencent à circuler
Le 27 mai, Thomas Bloom, Will Sawin, Carl Schildkraut et Dmitrii Zhelezov ont publié un contre-exemple à la conjecture somme-produit sur les nombres réels. En gros, cette conjecture porte sur l’ampleur de l’ensemble obtenu lorsqu’on additionne ou multiplie les éléments d’un ensemble donné. Leur construction permet que les deux ensembles obtenus restent plus petits que l’échelle presque quadratique prévue par la conjecture. Les auteurs disent explicitement que le contre-exemple sur les distances unitaires les a incités à reconsidérer les corps de nombres de grand degré. Ils expliquent aussi que leur construction finale nécessite moins de théorie des nombres que le résultat antérieur. L’article somme-produit.
C’est un exemple concret de résultat issu de l’IA qui stimule des travaux mathématiques rédigés par des humains. Cela ne prouve pas qu’une IA a écrit l’article de suivi, et nous ne devons pas effacer ses auteurs en incorporant leurs travaux au bilan de réussite d’un laboratoire.
Le préimprimé de Cosmin Pohoata, soumis pour la première fois le 11 juin puis révisé le 28 juin, prolonge cette séquence vers le problème d’Elekes-Rónyai. Il donne un exemple polynomial dont les valeurs sur certains ensembles croissent moins que prévu, en s’appuyant sur des éléments des constructions récentes sur les distances unitaires et somme-produit. L’article établit explicitement le lien entre ces problèmes. L’article de Pohoata.
Le 6 juillet, Sungchul Lee, Pohoata et Daniel Zhu ont publié un nouveau résultat sur la grille de Minkowski. Leur construction préserve des propriétés de distances répétées dans des sous-ensembles, avec des conséquences pour les questions portant sur les distances répétées et les triangles isocèles. Cette structure est plus riche que la simple présentation d’une configuration exceptionnellement dense, sans examiner son comportement interne. L’article sur la grille de Minkowski.
La lecture optimiste trouve ici des éléments à l’appui. Le résultat de mai a fourni, en quelques semaines, une matière que d’autres chercheurs ont pu modifier et réutiliser. Nous proposons de mesurer la réussite à la production de méthodes de ce type, ainsi qu’au travail nécessaire pour les comprendre. Un simple décompte des problèmes résolus ne ferait pas ressortir cette différence.
Juillet : le contre-exemple jacobien montre pourquoi la portée compte
Un deuxième épisode marquant concerne la conjecture jacobienne. Dans son exposé du 21 juillet, Terence Tao examine un contre-exemple produit avec Fable AI : une application polynomiale de trois variables complexes qui est inversible dans un petit voisinage, mais envoie globalement des points distincts sur une même image. L’affirmation générale de la conjecture échoue en trois dimensions et plus ; le cas bidimensionnel demeure ouvert. Tao donne des formules explicites et explique la géométrie de la construction. L’exposé mathématique de Tao.
Un contre-exemple explicite peut rendre sa contradiction essentielle relativement accessible au calcul. Découvrir pourquoi un tel exemple devrait exister et comment en construire d’autres du même type exige un travail mathématique supplémentaire. L’épisode de la conjecture jacobienne permet au lecteur de voir ces tâches distinctes présentées dans des publications.
Cette distinction a continué de compter en septembre. Dans son préimprimé du 15 septembre, Arno van den Essen présente une méthode élémentaire pour trouver un contre-exemple équivalent, après des changements linéaires de coordonnées, à l’exemple découvert par Levent Alpöge. Il s’agit d’une nouvelle explication de la construction, et non d’une deuxième réfutation indépendante de la conjecture initiale. L’article de van den Essen.
Pour un responsable de recherche, cela suggère un changement pratique dans les critères de reconnaissance. Financer la personne qui rend une découverte complexe compréhensible peut débloquer autant de travaux ultérieurs que financer une nouvelle recherche d’un résultat spectaculaire. C’est notre appréciation de cette séquence, et non l’affirmation que les universités ont déjà modifié leurs incitations.
Août : un éventail plus large de résultats mathématiques
La publication d’OpenAI du 1er août présentait dix groupes de résultats en mathématiques et en informatique théorique. L’entreprise affirme qu’une version interne d’Astra a produit les arguments ; des humains ont travaillé avec le modèle à la préparation des manuscrits, et le modèle a produit des certificats Lean. Le récit de production diffère de l’annonce d’un résultat unique en mai et explicite le rôle de la préparation des manuscrits par des humains. L’annonce d’août.
La collection associée, mise à jour le 6 août, présente les résultats suivants. Il s’agit des descriptions données par les manuscrits, et non de dix certifications indépendantes de BIG CHANGE :
- Empilement de sphères : une borne asymptotique supérieure plus précise en grandes dimensions.
- Codes binaires et sphériques : des limites renforcées sur la taille des codes pour des séparations données.
- Théorie des groupes : construction d’un groupe non sofic.
- Algèbres d’opérateurs : des contre-exemples à la conjecture de rigidité de Connes.
- Complexité arithmétique : des bornes inférieures renforcées pour les circuits et les formules appliqués au permanent.
- Jeux quantiques : un théorème d’amplification parallèle exponentielle.
- Problèmes de réseaux : des résultats plus solides sur la difficulté d’approximation du problème du vecteur le plus proche.
- Géométrie convexe : une preuve de la conjecture de volume d’Ehrhart.
- Théorie de Ramsey : une borne inférieure superexponentielle pour les nombres de Ramsey des triangles multicolores.
- Théorie extrémale des graphes : des contre-exemples aux conjectures de compacité et de dégénérescence.
La collection de recherche sur les dix résultats.
La diversité des résultats compte, mais elle rend aussi trompeur tout bilan unique. Trouver un contre-exemple, améliorer une borne et démontrer un théorème général n’ont pas les mêmes conséquences. Et un résultat sur la difficulté d’un problème mathématique ne démontre pas automatiquement une attaque contre un système cryptographique déployé. Les applications exigent leur propre enchaînement de raisonnements et d’éléments de preuve.
Le 10 août, Anthropic a publié une avancée plus ciblée en lien avec l’hypothèse de Riemann. L’entreprise indique qu’un modèle Claude non publié a amélioré la borne inférieure de la proportion de zéros de la fonction zêta situés sur la droite critique. Les mathématiciens d’Anthropic ont examiné le travail, des spécialistes externes ont évalué l’article et une formalisation a été produite. L’entreprise précise que Claude n’a pas résolu l’hypothèse de Riemann et que ces techniques ne devraient pas y parvenir. Le récit d’Anthropic.
L’article associé indique une borne légèrement supérieure aux deux tiers, soit environ 67,25 %, et précise les résultats analytiques antérieurs sur lesquels il s’appuie. Il s’agit d’un énoncé mathématique asymptotique, et non de l’affirmation que la vérification d’un grand échantillon fini de zéros prouve l’hypothèse. Cette distinction est essentielle : une borne inférieure sur la proportion ne situe pas tous les zéros concernés sur la droite. Le manuscrit sur les zéros de la fonction zêta.
D’autres manuscrits ambitieux circulent également. Un document hébergé sur le site d’Alpöge propose une structure complexe sur la sphère de dimension six. Sa construction peut être examinée, mais la copie consultée ne permet pas d’établir une date d’annonce fiable ni de décrire complètement la contribution de l’IA. Nous l’incluons donc comme une proposition que les lecteurs peuvent étudier, sans la présenter comme une étape indépendamment établie de cette chronologie. Le manuscrit sur la sphère de dimension six.
Début septembre : les écarts entre nombres premiers mettent en évidence les limites de la vérification
La série d’annonces a aussi porté sur les écarts entre nombres premiers. Un article préliminaire du 3 septembre issu de la collaboration Axiom affirme qu’il existe une infinité de paires de nombres premiers consécutifs distants d’au plus 212. Il attribue les travaux analytiques à Julia Stadlmann et s’appuie sur le projet Polymath antérieur. Son certificat Lean prend également pour hypothèses des estimations analytiques et un certificat variationnel vérifié séparément. Ce résultat fait progresser la question des écarts bornés ; la conjecture des nombres premiers jumeaux exige une infinité d’écarts égaux à deux. L’article de l’équipe Axiom.
Le dépôt public PrimeGaps186 d’OpenAI présente une borne encore plus petite, assortie d’une réserve cruciale. Son développement Lean dépend de trois axiomes d’entrée qui couvrent deux estimations tirées de la littérature et des bornes numériques sur des intégrales. Le dépôt précise que le certificat numérique ne démontre pas ces axiomes. Les lecteurs doivent donc distinguer l’argument mathématique proposé de la partie vérifiée formellement sous les hypothèses indiquées. Il serait inexact de décrire cet artefact comme une preuve complète et inconditionnelle à partir des seuls axiomes fondamentaux. Le dépôt PrimeGaps186.
Un autre manuscrit d’OpenAI porte sur les grands écarts : la taille que peuvent atteindre les intervalles entre nombres premiers consécutifs. Il présente une amélioration de la borne inférieure du plus grand écart sous un seuil croissant. Il s’agit d’une question extrémale distincte de celle de l’existence d’une infinité de paires de nombres premiers rapprochés ; les progrès sur l’une ne doivent pas être comptés comme une solution à l’autre. Le manuscrit sur les grands écarts.
Ces détails rendent particulièrement instructif l’épisode des écarts entre nombres premiers. Deux nombres dans un titre peuvent donner l’impression d’une simple course. Lorsque les dépendances de la preuve deviennent visibles, la meilleure question est de savoir quelles étapes ont été établies et par quelles méthodes. Rendre les hypothèses explicites est utile même lorsqu’une formalisation reste incomplète.
4 septembre : la formalisation fait partie de l’histoire de la découverte
L’annonce d’Anthropic du 4 septembre concerne un théorème dont la preuve mathématique était déjà connue : le dernier théorème de Fermat. La réalisation annoncée est une formalisation complète en Lean, produite en grande partie de façon autonome par Claude en onze jours. L’entreprise décrit le pilotage humain et une plateforme de collaboration qui a aidé les agents à suivre les dépendances. Elle reconnaît la tradition de preuves mathématiques sur laquelle repose le travail. L’annonce sur la formalisation.
Le dépôt public fournit des éléments plus précis que le titre. Il énonce le théorème, consigne les dépendances et documente les vérifications par rapport aux axiomes standard de Lean et à la version de l’énoncé utilisée par Mathlib. Il se présente aussi comme un artefact de recherche non maintenu. Nous avons consulté cette documentation, mais nous n’avons pas relancé sa compilation. Le dépôt sur le dernier théorème de Fermat.
Si les outils qui produisent davantage d’arguments candidats peuvent aussi aider à les formaliser, la capacité de vérification peut elle aussi augmenter. C’est une raison importante d’être optimiste. Les chercheurs ultérieurs disposent d’éléments concrets à examiner. Ils doivent encore savoir si les résultats intermédiaires sont faciles à réutiliser, si les dépendances restent compilables et qui assure la maintenance de l’artefact. Le volume de code généré ne permet pas, à lui seul, de répondre à ces questions.
Les institutions ont ici un choix utile à faire. Un laboratoire peut publier une preuve comme démonstration finale de son modèle, ou la soutenir en tant qu’infrastructure destinée au travail d’autres personnes. Ces démarches entraînent des obligations différentes après le lancement. La maintenance, les exemples explicatifs et les références stables devraient faire partie du budget de recherche.
8 septembre : ce qu’affirme réellement le résultat sur Navier-Stokes
Le résultat sur les fluides met ces questions encore davantage en évidence. Dans son annonce du 8 septembre, mise à jour le 10, OpenAI présente une solution proposée au problème d’existence et de régularité de Navier-Stokes. L’entreprise attribue les travaux à un modèle interne fonctionnant avec des agents coordinateurs, et publie un argument écrit ainsi qu’une formalisation Lean. OpenAI affirme ne pas vouloir réclamer le prix du millénaire. L’annonce.
Le manuscrit traite du mouvement d’un fluide incompressible en trois dimensions, avec une viscosité positive et une force extérieure construite avec soin. Partant du repos, la solution proposée développe une vitesse non bornée en temps fini, tandis que son énergie totale reste bornée. La force est régulière et localisée dans l’espace et le temps. Sa construction mathématique s’appuie sur un vortex qui s’effondre et sur des corrections organisées de façon à préserver la régularité de la force résiduelle. Il s’agit d’affirmations concernant des solutions d’équations, et non d’observations issues d’une expérience physique ou d’un nouveau simulateur d’ingénierie. Le manuscrit sur Navier-Stokes.
La force extérieure est essentielle pour comprendre la portée du résultat. La description officielle du problème par Charles Fefferman autorise une force régulière dans les cas de perte de régularité C et D. Les cas A et B portant sur la régularité globale concernent les équations sans force extérieure. Un résultat valide du type proposé peut donc traiter un cas explicitement autorisé par le problème Clay, tout en laissant sans réponse la question de la régularité globale sans force extérieure. Qualifier la force de sans importance exagérerait le théorème ; affirmer qu’elle est hors du cadre du problème déformerait les règles. L’énoncé officiel du problème.
OpenAI a aussi publié un argument distinct sur les équations d’Euler, qui décrivent un fluide idéalisé sans viscosité. Ce manuscrit propose une perte de régularité en temps fini à partir de données initiales régulières et sans force extérieure. Les équations d’Euler et de Navier-Stokes sont apparentées, mais il faut distinguer les hypothèses et les conclusions de ces deux articles. Le manuscrit sur Euler.
Le contexte historique de ces recherches compte. Dans sa déclaration du 10 septembre, la Société mathématique européenne reconnaît les travaux de Córdoba, Martínez-Zoroa et Zheng, ainsi que ceux d’Alpöge et Buckmaster et d’autres contributions mathématiques antérieures. Elle soulève aussi des questions d’accès, d’auteurs et de reconnaissance. Un récit qui passerait directement du nom d’un modèle à un théorème effacerait l’accumulation d’idées qui a rendu ce travail possible. La déclaration de la Société mathématique européenne.
Le 11 septembre, l’Institut de mathématiques Clay a réagi avec un enthousiasme mesuré à ce qui semble être une résolution, et indiqué que son évaluation ainsi que l’attribution du mérite suivraient un processus volontairement lent. C’est une réponse institutionnelle importante. Ce n’est ni l’attribution d’un prix ni une déclaration selon laquelle tous les aspects des travaux ont achevé leur évaluation. L’annonce de Clay.
Pour le lecteur, la conclusion exacte est déjà substantielle sans rien y ajouter : un laboratoire d’IA a publié une preuve proposée portant sur un problème du millénaire reconnu, accompagnée d’artefacts mathématiques et formels que l’on peut examiner, et de grandes institutions prennent le résultat au sérieux. L’acceptation plus large, l’attribution du mérite et la compréhension restent des processus qui demandent encore du travail.
La vérification d’une preuve répond à une question précise
La vérification formelle modifie les éléments dont disposent les personnes chargées de l’évaluation. Elle devrait aussi permettre une plus grande précision dans la couverture médiatique.
La documentation de Lean distingue la validité d’une preuve du sens de l’énoncé démontré. Une vérification réussie de base établit qu’un énoncé formel découle de ses définitions et de ses hypothèses. Des contrôles supplémentaires peuvent révéler les dépendances inachevées, auditer les axiomes et comparer la preuve à un énoncé spécifié de manière indépendante. La documentation décrit des vérifications renforcées utilisant des vérificateurs externes, tout en signalant les hypothèses restantes. Le guide de validation de Lean.
Imaginons un chercheur qui a besoin d’une borne valable pour toutes les entrées d’un algorithme. Un assistant fournit un théorème formellement correct, mais sa définition des entrées admissibles exclut une catégorie difficile. La preuve peut être correcte alors que l’application du chercheur reste sans fondement. Cet exemple hypothétique montre pourquoi il faut examiner la traduction de la question en son énoncé formel.
La nouveauté exige un autre type de vérification. Un système de preuve ne permet pas d’établir si le même argument figurait déjà sous une autre terminologie dans un article antérieur, si les attributions sont complètes ou si l’amélioration annoncée change quelque chose d’important pour une application. Ces jugements exigent une recherche bibliographique et une expertise du domaine.
Nous demanderions donc à un laboratoire qui publie un résultat majeur de fournir un dossier durable : l’affirmation exacte en langage mathématique courant, son équivalent formel lorsqu’il existe, la preuve et ses dépendances, une description claire des contributions humaines et du modèle, et un registre des éléments examinés et révisés. C’est la norme de publication que nous proposons. Elle permet aux autres chercheurs de déterminer les responsabilités et de reproduire les vérifications concernées.
Le groupe consultatif s’attaque à un problème croissant de coordination
L’annonce du 21 septembre du Groupe consultatif sur les mathématiques et l’intelligence artificielle intervient dans ce contexte. Le groupe se dit indépendant, non rémunéré et prêt à conseiller toute entreprise concernée par l’IA. Sa tâche immédiate consiste à conseiller OpenAI sur la publication d’autres résultats que l’entreprise affirme avoir obtenus. Il promet des recommandations publiques et précise ne disposer d’aucun pouvoir décisionnel au sein des entreprises. L’annonce publiée sur le blogue de Terence Tao est un billet invité rédigé par le groupe. La déclaration du groupe.
OpenAI décrit un mandat portant sur l’évaluation, la communication, la portée et la diffusion. L’entreprise précise aussi que le groupe n’a pas pour rôle de conseiller le rythme de ses travaux mathématiques internes. Il faut donc comprendre ce rôle consultatif comme un canal d’examen et de coordination, les décisions restant du ressort de l’entreprise. L’annonce d’OpenAI sur le groupe consultatif.
Cette organisation a des avantages. Une meilleure coordination peut réduire le dédoublement du travail d’évaluation, aider à trouver les spécialistes compétents et faire en sorte que la description d’un résultat corresponde aux éléments qui l’étayent. Ses limites sont tout aussi claires : les conseils appellent une réponse, et l’indépendance seule ne permet pas de les faire appliquer. Les lecteurs devraient suivre les recommandations publiées et la manière dont les entreprises y donnent suite.
La critique porte aussi sur la finalité de la recherche. Dans leur déclaration du 11 septembre, les auteurs de « Mathématiques et IA : un grave désalignement de l’IA en mathématiques » soutiennent qu’une course à la résolution de problèmes répertoriés peut négliger le développement de la compréhension et la formation des futurs mathématiciens. Les signataires évoquent un risque pour les processus qui rendent les idées transmissibles et utiles. Il s’agit d’une position sérieuse de personnes travaillant dans la discipline, et non d’une mesure démontrant que tous les usages de l’IA lui ont déjà nui. La déclaration.
Dans un essai invité publié le 15 septembre sur le blogue de Tao, Henry Cohn développe un argument connexe : des résultats mal expliqués peuvent imposer un lourd travail à la communauté qui doit les assimiler. Il s’inquiète aussi des incitations destinées aux personnes qui effectuent ce travail d’explication. L’attribution du mérite compte ici également : cet essai est de Cohn, même s’il est hébergé par Tao. L’essai de Cohn.
La prochaine avancée devrait être plus facile à utiliser pour d’autres
La séquence de mai à septembre étaye un récit optimiste par des exemples concrets. Un contre-exemple géométrique a inspiré d’autres constructions. Des chercheurs ont trouvé des moyens plus clairs d’expliquer une application polynomiale surprenante. La formalisation a produit des artefacts supplémentaires qui permettent d’examiner un raisonnement complexe. Les ingrédients d’une relation féconde entre les résultats des modèles et les pratiques mathématiques sont visibles.
Le scénario pessimiste est tout aussi concret. Les laboratoires pourraient produire des résultats proposés plus vite que d’autres ne peuvent les comprendre, puis compter les annonces comme des contributions scientifiques achevées. Le travail d’évaluation pourrait devenir une charge imposée à un petit groupe de spécialistes, tandis que les ressources et le prestige iraient aux systèmes qui produisent cet arriéré. Un accès restreint aux modèles pourrait accentuer le déséquilibre entre ceux qui génèrent des découvertes et ceux à qui revient la tâche de les évaluer.
Nous estimons que les laboratoires, les bailleurs de fonds et les revues devraient mesurer les deux versants du processus. Il faut suivre les découvertes candidates, mais aussi l’examen indépendant, les simplifications utiles, les arguments corrigés, les bibliothèques formelles réutilisables et les travaux qui en découlent. Il faut reconnaître le mérite des personnes qui rendent un résultat intelligible. Il faut publier les corrections avec la même persistance que les annonces.
Pour le lecteur qui cherche à suivre la prochaine percée, la question la plus révélatrice est précise : que peut désormais faire un autre chercheur qu’il ne pouvait pas faire auparavant ? Il peut s’agir de construire un contre-exemple, d’établir une garantie plus forte, de vérifier un argument difficile ou d’enseigner une nouvelle méthode. C’est là que les progrès de l’IA en mathématiques deviennent des progrès mathématiques.
