722 démonstrations d’une IA : ce que l’on peut déjà vérifier

Dans la nuit du 6 au 7 octobre, déjà au petit matin en Espagne, OpenAI a mis en ligne sur GitHub 722 manuscrits de mathématiques. Ils ont été écrits par un modèle interne que l’entreprise n’a ni publié ni nommé, et ils se regroupent en 372 « familles » : chacune réunit un résultat principal avec ses variantes et ses conséquences. OpenAI explique qu’elle évalue ses modèles sur des problèmes de recherche non résolus et qu’elle a publié les résultats qui atteignaient un niveau de pertinence suffisant.

Le 21 septembre, l’entreprise avait affirmé que son modèle avait résolu « plus de cent » problèmes ouverts, sans en montrer aucun. Elle les a maintenant montrés, et ils sont plus nombreux. On y trouve des affirmations qui, si elles se confirment, refermeraient des questions ouvertes depuis des décennies : sur la répartition des nombres premiers, sur les limites des algorithmes d’optimisation ou sur la raison pour laquelle un aimant reste un aimant.

Lance Fortnow, un vétéran de l’informatique théorique, a écrit le lendemain que son domaine avait davantage progressé en 24 heures qu’au cours des trois décennies précédentes réunies. Dans le même billet, il ajoutait que rien de tout cela n’est encore vérifié.

Cette réserve est la question de cet article : que signifie, pour ces résultats, être « vérifiés » ? Cette fois, une machine peut en contrôler une partie, ce qui n’était le cas pour aucune annonce précédente. Mais ce contrôle comporte plusieurs niveaux, et l’essentiel du travail reste à faire.

Ce que contient exactement le dépôt

D’après le README du dépôt, le modèle a reçu environ 4 000 problèmes, et chaque résultat a consommé en moyenne une puissance de calcul équivalente à trois heures de raisonnement de ChatGPT Pro. L’entreprise n’explique pas comment elle a choisi ces problèmes, mais elle laisse voir une proportion : environ 4 000 tentatives ont donné 372 familles. Comme le souligne Fortnow, le modèle a résolu moins de 10 % de ce qu’on lui a soumis.

Presque tout a été obtenu avec la même procédure automatique. Le README reconnaît deux exceptions, sans les détailler : une région de la fonction zêta de Riemann dépourvue de zéros et la conjecture de Hodge pour une certaine famille d’objets géométriques. Ce sont précisément les deux résultats les plus proches de problèmes du millénaire. L’un des textes sur la fonction zêta a en outre été retouché par des personnes pour le rendre lisible.

Le dépôt comprend :

• les articles en PDF avec leurs sources ;
• dix résumés abrégés du raisonnement suivi par le modèle ;
• une bibliothèque de démonstrations formelles en Lean, dont nous parlerons plus loin ;
• et un engagement à conserver l’historique : les corrections seront publiées sous forme de nouvelles versions, sans effacer les précédentes.

Le README lui-même prévient : « Some of the unformalized results could have issues ». Certains des résultats non formalisés pourraient présenter des problèmes.

Le billet d’annonce ne met en avant aucun résultat précis. La liste de « grands résultats » qui circule ces jours-ci est une sélection faite par la presse et par les mathématiciens eux-mêmes. Nous en avons retenu quatre qui permettent de mesurer l’ampleur de ce qui est affirmé.

Quatre résultats pour comprendre l’enjeu

Les nombres premiers et la fonction zêta

Les nombres premiers semblent se répartir sans ordre, mais ils suivent une loi moyenne démontrée en 1896 : jusqu’à un nombre x, il y a environ x/ln x nombres premiers. La question intéressante est de savoir de combien le décompte réel s’écarte de cette loi. Et la réponse dépend de l’emplacement des zéros de la fonction zêta de Riemann, les points où cette fonction s’annule.

L’hypothèse de Riemann, formulée en 1859 et l’un des sept problèmes du millénaire, affirme que tous ces zéros se trouvent sur une droite précise, celle de partie réelle 1/2. Si elle est vraie, l’erreur commise en comptant les nombres premiers est la plus petite possible. Jusqu’à aujourd’hui, on savait seulement qu’il n’y a pas de zéros exactement sur le bord, en partie réelle 1, ni dans une bande qui se rétrécit à mesure que l’on monte. Personne n’avait réussi à démontrer qu’il existe une bande de largeur fixe sans zéros. Cette version affaiblie est ce que l’on appelle l’hypothèse quasi-Riemann.

OpenAI affirme l’avoir démontrée : il n’y a pas de zéros de partie réelle supérieure à 7/8. Ce n’est pas l’hypothèse de Riemann, qui exige d’atteindre 1/2, mais ce serait la première avancée de ce type depuis que la question a été posée. Un autre manuscrit de la même famille exclut en outre les zéros dits de Siegel, une anomalie hypothétique qui oblige de nombreux théorèmes sur les nombres premiers à dépendre de constantes que personne ne sait calculer. Un second manuscrit démontre une région un peu plus petite, à partir de 11/12, par une autre voie. C’est le texte qu’ont retouché des personnes.

Les limites des algorithmes d’optimisation

De nombreux problèmes pratiques sont trop difficiles pour être résolus de façon exacte à grande échelle. Un exemple : diviser un réseau en deux groupes de manière à couper le plus grand nombre possible de connexions (Max-Cut). Un autre : choisir le plus petit nombre de nœuds qui touchent toutes les connexions (Vertex Cover). Dans ces cas, nous utilisons des algorithmes qui donnent une réponse approchée avec une qualité garantie. Celui de Max-Cut, par exemple, assure au moins 87,8 % de l’optimum.

Depuis 2002, la conjecture des jeux uniques (Unique Games), de Subhash Khot, prédit que l’on ne peut pas faire mieux en un temps raisonnable. Si elle est vraie, beaucoup des algorithmes approchés que nous utilisons déjà seraient les meilleurs possibles, sauf si P = NP. OpenAI affirme avoir démontré la conjecture. Par ailleurs, dans un résultat distinct, elle affirme prouver, sans s’appuyer sur cette conjecture, qu’améliorer ces garanties pour Max-Cut et Vertex Cover est NP-difficile, c’est-à-dire aussi difficile que les problèmes les plus durs de leur classe.

Il y a ici une histoire humaine. Selon Quanta Magazine, des rumeurs selon lesquelles OpenAI détenait la démonstration ont commencé à circuler le 11 septembre. Dor Minzer (MIT) et deux étudiants travaillaient depuis sept ans sur une variante du problème et l’avaient résolue en avril. Trois jours après les rumeurs, ils ont publié 95 pages avec un avertissement dès la première : le texte était mathématiquement complet, mais il n’avait pas la forme sous laquelle ils voulaient le partager. « There is a lot of value in failing and knowing why you failed », a déclaré Minzer au magazine : échouer et comprendre pourquoi a beaucoup de valeur.

Pourquoi un aimant reste un aimant

Dans un aimant, les petits moments magnétiques des atomes, les spins, s’alignent. La physique quantique décrit ce comportement avec le modèle de Heisenberg, et tout physicien tient pour acquis qu’en trois dimensions, à basse température, le matériau conserve son aimantation. Le démontrer rigoureusement était une autre affaire. La version classique du modèle et le cas quantique antiferromagnétique, où les spins voisins pointent dans des sens opposés, ont été résolus il y a des décennies. Mais la technique qui a fonctionné dans ces cas ne s’applique pas à l’aimant quantique ordinaire, et Elliott Lieb l’a inscrit en 1999 comme « Problem A » d’une liste de problèmes ouverts de physique mathématique.

OpenAI affirme l’avoir démontré pour toutes les dimensions à partir de trois. C’est un bon exemple d’un type de résultat qui passe souvent inaperçu : il ne change pas ce que nous croyons sur le monde, mais il transforme une certitude physique en théorème.

Une question classique à la réponse inattendue

À partir d’un « groupe libre », l’ensemble de tous les mots que l’on peut écrire avec deux lettres et leurs inverses, ou avec trois, on construit un objet d’analyse appelé facteur de von Neumann. Ces objets apparaissent dans les travaux fondateurs de Murray et von Neumann, et la question, attribuée à Richard Kadison, est de savoir si l’objet se souvient du nombre de lettres avec lequel on a commencé. Elle est considérée comme le problème ouvert le plus connu de son domaine, et une bonne partie de la recherche s’est attachée à démontrer que les objets étaient différents.

OpenAI affirme le contraire : avec deux lettres ou avec trois, on obtient le même objet. Si cela se confirme, ce serait l’un de ces résultats qui obligent à revoir l’intuition de tout un domaine. Il illustre en outre bien le problème dont traite la section suivante.

Le reste du catalogue

Ces quatre résultats ne sont qu’un échantillon. Le tableau rassemble d’autres résultats de premier plan et indique s’ils ont une démonstration formelle en Lean :

Source : catalogue du dépôt et catalogue des formalisations, consultés le 7 octobre 2026. Descriptions simplifiées par Codin.

« Vérifié » peut vouloir dire trois choses différentes

La nouveauté de cette publication par rapport aux précédentes, c’est Lean. Lean est un langage dans lequel on écrit une démonstration avec un tel niveau de détail qu’un programme peut la contrôler pas à pas, sans faire confiance à personne. Il s’appuie sur Mathlib, une bibliothèque communautaire de définitions et de théorèmes déjà vérifiés. Qu’une démonstration « compile » en Lean signifie que chaque étape découle des précédentes.

Mais lorsqu’on dit qu’un résultat est vérifié, il convient de distinguer trois questions.

Première : la démonstration formelle est-elle correcte ?

C’est ce que tranche Lean, et cela peut être refait en dehors d’OpenAI. Le dépôt inclut des défis pour Comparator, un outil qui n’accepte une démonstration que si elle prouve exactement l’énoncé de référence et n’utilise que les axiomes standard. Quelques heures après la publication, plusieurs personnes extérieures à OpenAI ont recompilé la démonstration de la région 7/8 sur leurs machines, avec un résultat correct.

Le dépôt contient plus de 120 000 fichiers Lean, mais cette bibliothèque ne couvre qu’une petite partie du catalogue : 162 des 722 manuscrits ont leur résultat principal formalisé.

Deuxième : l’énoncé formel dit-il ce que nous croyons ?

Lean garantit que la démonstration prouve l’énoncé qu’on lui a fourni. Il ne garantit pas que cet énoncé signifie ce que dit l’article. C’est le niveau qui dépend le plus des personnes, et sa difficulté varie beaucoup d’un résultat à l’autre.

Dans le meilleur des cas, l’énoncé est si court que toute personne ayant un peu de formation peut le lire :

theorem riemannZeta_ne_zero_of_seven_eighths_lt_re
    {s : ℂ} (hs : (7 / 8 : ℝ) < s.re) : riemannZeta s ≠ 0 := by
  sorry

Si la définition est celle de la communauté et que l’énoncé tient en deux lignes, la confiance qu’apporte Lean est très élevée. C’est pourquoi la région sans zéros de 7/8 est, aujourd’hui, le résultat le mieux vérifié du catalogue.

Le cas des facteurs de groupes libres est différent. Mathlib ne contient pas encore ces objets, si bien que le défi Comparator les définit à partir de zéro, avec des définitions elles aussi écrites par OpenAI. Avec Unique Games, il se passe quelque chose de semblable : l’énoncé repose sur des milliers de caractères d’encodages propres. Une démonstration parfaite d’une définition légèrement erronée démontre autre chose. Quelqu’un qui connaît le domaine doit lire ces définitions et confirmer qu’elles capturent le vrai problème.

Le catalogue des formalisations le dit clairement dans deux champs : les démonstrations en Lean ont elles aussi été écrites par un agent d’IA (automation: agent), et leur relecture figure comme en attente (review: unchecked).

Troisième : qu’avons-nous compris ?

Même lorsque l’énoncé est bien formalisé, Lean ne couvre souvent que le théorème principal. Pour l’hypothèse quasi-Riemann, la documentation elle-même prévient que les applications de l’article ne sont pas incluses. Or ces applications sont précisément ce qui intéresse un spécialiste des nombres premiers.

Les 560 autres manuscrits dépendent aujourd’hui de leur texte en langage naturel et du jugement interne d’OpenAI. Parmi eux figure la conjecture de Hodge, l’un des deux résultats qui n’ont pas suivi la procédure automatique, et qui n’a pas de formalisation.

Reste ensuite ce qu’aucun programme ne contrôle : quelle idée fait fonctionner chaque démonstration, si elle ouvre de nouvelles voies et ce qu’elle change dans le domaine. Nous avons déjà parlé de ce déplacement dans quand démontrer cesse d’être le goulot d’étranglement. Cette publication le rend tangible : la machine a rendu le premier niveau beaucoup plus facile, et le travail humain se concentre sur les deux autres.

Ce qu’ont demandé les mathématiciens et ce qui est arrivé

Le 21 septembre, OpenAI a présenté un groupe consultatif indépendant de neuf mathématiciens, AGMAI, basé à l’Institute for Advanced Study de Princeton. Le 29 septembre, une semaine avant la publication, le groupe a publié ses recommandations, fondées sur plus de 600 réponses de la communauté. Elles commençaient par une demande : que les laboratoires cessent de tester des problèmes mathématiques avancés avec des modèles propriétaires. Voici la comparaison entre ce qui était demandé et ce qui est arrivé :

Sources : recommandations d’AGMAI du 29 septembre, annonce d’OpenAI et README du dépôt. Comparaison établie par Codin.

Sans le modèle ni les prompts, personne ne peut reproduire la manière dont chaque résultat a été obtenu. Cela n’empêche pas de vérifier une démonstration, qui tient ou ne tient pas par elle-même. Mais cela empêche de savoir quel poids a eu le choix des problèmes, ce qui a été tenté sans succès ou si les deux exceptions ont reçu une aide dont les autres résultats n’ont pas bénéficié.

Le 6 octobre également, AGMAI a publié une déclaration qu’il vaut la peine de lire en entier. Elle indique que son rôle consultatif ne doit pas être interprété comme une évaluation de l’impact de ces résultats ni comme une caution du processus. Elle ajoute qu’il revient à la communauté de juger dans quelle mesure ses recommandations ont été suivies. Et elle le résume ainsi : « This release is the beginning, not the completion, of the process ». La publication est le début du processus de compréhension et d’intégration de ces résultats, pas sa fin.

Comment la communauté l’a accueillie dans les premières heures

Au 7 octobre, aucun spécialiste n’avait publié d’examen d’un résultat précis, et aucune erreur n’avait été confirmée. Ce qui existe, ce sont des positions sur la manière de lire l’annonce.

Andrew Sutherland (MIT) a demandé dans Scientific American de traiter comme non vérifié ce qui ne peut pas être reproduit : « We should ask for receipts », autrement dit, il faut exiger des preuves. Daniel Litt (Université de Toronto) a répondu dans le même article avec l’argument inverse. Si nous voulons connaître les réponses, cela n’a pas de sens de demander à l’entreprise de les garder secrètes, et il pense que ce sera bon pour les mathématiques. Mark Braverman (Princeton) a déclaré à Quanta que les mathématiques par communiqué de presse ne sont « pas très saines », tout en reconnaissant qu’une telle démonstration peut ouvrir de nouvelles pistes.

Entre-temps, la vérification a commencé à s’organiser en dehors d’OpenAI. Outre les recompilations Lean, un catalogue communautaire de problèmes ouverts a importé des centaines de résultats avec le même avertissement pour chacun : aucun mathématicien indépendant ne l’a encore examiné. Il en signale déjà plusieurs comme contestés, en raison de possibles conflits avec des résultats publiés auparavant.

Le ton de fond a deux faces. Il y a de l’étonnement devant l’ampleur, y compris chez les critiques. Et il y a de la lassitude : après la polémique sur la paternité de Navier–Stokes et la lettre des médaillés Fields, la critique ne vise plus seulement ce que disent ces systèmes. Elle vise aussi qui décide du rythme et la manière dont on publie.

Un test au vert ne prouve que ce que le test vérifie

Le 29 septembre, nous avons soutenu que qui annonce cent avancées devrait accompagner chacune d’informations suffisantes pour la vérifier et bâtir dessus. Cette publication en apporte bien plus que la précédente. Il y a des manuscrits complets, une bibliothèque formelle que n’importe qui peut exécuter et un historique des versions. Il serait injuste de ne pas le reconnaître. Mais il manque toujours ce qui permettrait de reproduire le processus, et on ne sait toujours pas clairement qui paie le travail de relecture.

Dans le logiciel, nous connaissons bien la distinction que ce cas rend visible. Que les tests passent ne prouve pas que le programme fait ce qu’il faut : cela prouve qu’il fait ce que les tests vérifient. Si la spécification est mal écrite, le code peut la respecter à la perfection et ne servir à rien pour autant. Lean a fait de la correction d’une démonstration quelque chose qui ressemble à un test automatique, rapide et fiable. La question s’est déplacée vers la spécification : l’énoncé formel est-il bien le problème qui nous importe, et que nous apprend la démonstration, au-delà du fait qu’elle est vraie ?

C’est pourquoi le chiffre à suivre dans les prochains mois n’est pas 722. Trois autres en diront davantage :

• Combien d’énoncés formels sont relus par quelqu’un du domaine, en commençant par ceux qui reposent sur des définitions propres.
• Combien de résultats de premier plan font l’objet d’un examen par des spécialistes, surtout ceux qui n’ont pas de Lean, comme Hodge.
• Combien de corrections enregistre l’historique des versions. Un dépôt de cette ampleur sans erreurs serait plus suspect qu’un dépôt qui en contient.

Si ces chiffres augmentent, cette publication aura permis à la communauté d’intégrer des résultats réels. S’ils n’augmentent pas, nous aurons des centaines de théorèmes dont nous saurons seulement qu’une machine affirme qu’ils sont vrais.

Sources

• OpenAI : « Sharing AI progress in mathematics », 6 octobre 2026.
• Dépôt openai/math : README, catalogue des manuscrits, catalogue des formalisations, portée de la formalisation de l’hypothèse quasi-Riemann et défi Comparator. Commit adc7f124, consulté le 7 octobre 2026.
• AGMAI : recommandations du 29 septembre 2026 et déclaration du 6 octobre.
• Lance Fortnow : « Open No More », 7 octobre 2026.
• Quanta Magazine : la course à la conjecture des jeux uniques, 7 octobre 2026.
• Scientific American : réactions de Sutherland et Litt, 6 octobre 2026.
• Elliott Lieb : « Problem A », liste de problèmes ouverts de physique mathématique, 1999.
• Recompilations indépendantes de la région 7/8 : Zhang-Liao/quasi-riemann et davegoldblatt/openai-zeta-proof-check. Elles vérifient la démonstration formelle, pas l’article.
• Catalogue communautaire vibemathed : import des résultats d’OpenAI.

Note éditoriale : nous n’avons audité aucun des résultats. Les descriptions mathématiques sont simplifiées pour un lecteur non spécialiste et reflètent ce qu’affirme OpenAI, pas un consensus de la communauté.