722 preuves en un commit : ce que la publication mathématique d'OpenAI dit de l'avenir de la vérification

Le 6 octobre 2026, OpenAI a déposé sur GitHub 722 manuscrits mathématiques d'un modèle interne¹². Cédric Villani parle du changement le plus radical depuis quatre siècles, Yann LeCun d'une nouvelle ère. Le lendemain, OpenAI retirait trois de ces manuscrits : une erreur de signe dans l'un invalidait les deux autres³. Quand la machine génère à ce débit, la valeur se déplace de la génération vers la vérification. DSI, CTO, lead devs : ce dépôt est une maquette grandeur nature de ce qui attend vos agents.

Qu'y a-t-il dans le dépôt du 6 octobre ?

OpenAI a publié un billet court, « Sharing AI progress in mathematics » (une version française existe, en fr-CA), et un dépôt public, github.com/openai/math, sous licence Apache 2.0¹². Le README du commit initial annonce 722 manuscrits regroupés en 372 familles, tirés d'une évaluation portant sur environ 4 000 problèmes ouverts. Chaque résultat a consommé en moyenne l'équivalent de trois heures de « ChatGPT Pro thinking ». S'y ajoutent une bibliothèque Lean, dix résumés du raisonnement du modèle et un protocole de versions et de citations². Le New York Times a titré sur « 377 Math Problems », Quanta reprend ce total : les familles vont de 001 à 377, mais cinq numéros (045, 061, 070, 123, 163) restent vides, d'où les 372²¹².

OpenAI signale deux exceptions à sa procédure standard : le travail sur une région sans zéros de la fonction zêta, dont un humain a retouché la rédaction (la région Re(s) > 11/12) pour la lisibilité, et la conjecture de Hodge pour les variétés abéliennes de type CM². L'entreprise prévient que les résultats non formalisés peuvent contenir des erreurs. Un porte-parole a dit à Scientific American que presque chaque résultat vient d'un seul prompt à un seul agent, là où Navier-Stokes avait mobilisé en septembre un essaim de 10 000 agents¹⁶. Sam Altman a mis en avant quatre résultats : la quasi-hypothèse de Riemann, la conjecture des jeux uniques (Unique Games), un cas de la conjecture de Hodge et le problème des facteurs de groupes libres¹⁷.

Pourquoi trois manuscrits ont disparu en un jour

Le fichier history.md du dépôt raconte la suite³. Le 7 octobre, OpenAI retire trois manuscrits. Dans « Algebraicity of Weil classes on split abelian eightfolds », une erreur de signe invalide un argument, et avec lui la construction que deux papiers reprenaient : « Algebraicity of Kuga-Satake Correspondences for K3 Surfaces » et « The rational Hodge conjecture for products of K3 surfaces ». Le même jour, 14 autres manuscrits sont révisés (preuves réparées, énoncés corrigés, hypothèses clarifiées) et 13 mis à jour pour citer les nouvelles éditions. Le README affiche désormais 719 manuscrits en 372 familles, et 300 résultats principaux formalisés sur 719, soit environ 42 %². Le 722 du titre est celui du 6 octobre.

Je lis ce retrait comme la meilleure nouvelle de la semaine. Un signe faux, trouvé en un jour, et trois papiers qui tombent parce qu'ils partageaient une dépendance : la chaîne a cassé là où elle devait casser, et quelqu'un l'a vu. La génération avait produit l'erreur et ses deux conséquences sans la voir ; la vérification est le goulot. Et OpenAI a traité le retrait comme un changelog : notice datée, ancienne version archivée, rien de supprimé en silence.

Qui a recompilé les preuves, et avec quels outils ?

Le fait le plus utile de la semaine vient du forum développeurs d'OpenAI⁴. Dans les heures qui ont suivi la mise en ligne (message daté du 7 octobre, 01:52 UTC), un utilisateur, davegoldblatt, a publié une recompilation indépendante de la preuve Lean de la famille 003, ζ(s) ≠ 0 pour Re(s) > 7/8, exécutée à sa demande par un agent IA, Claude Code, en une seule passe sur une seule machine. L'outil Comparator du Lean FRO a accepté la preuve, puis un second noyau indépendant, nanoda, l'a confirmée face à un énoncé que l'auteur avait rédigé lui-même. Seuls les trois axiomes standard sont utilisés.

L'auteur pose lui-même les limites : la vérification porte sur la preuve Lean, sans toucher à l'article qui l'accompagne, et une seule exécution ne vaut pas reproduction. Il relève aussi qu'une seule des 405 configurations Comparator du dépôt initial active le second noyau⁴. Le même jour, un autre contributeur, selanavot, a étendu la borne ω ≤ 9/4 de la multiplication matricielle à tous les corps, avec Codex, preuve Lean à l'appui dans un fork⁴.

Pour Unique Games, Quanta (Ben Brubaker, 7 octobre) précise que la preuve de la conjecture 2-to-1 est vérifiée en Lean, sans édition humaine ni relecture par des experts indépendants¹².

Une preuve Lean qui compile dit-elle ce que le titre promet ?

Un article déposé sur arXiv le 6 octobre (arXiv:2610.08144, v1) par Alexander Bastounis, Fabian Circelli et Anders C. Hansen a pour titre « Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs »⁵. Les auteurs soutiennent que lever les ambiguïtés du langage naturel est, informellement, plus difficile que tout problème calculatoire, problème de l'arrêt compris ; l'autoformalisation par IA n'offre donc aucune garantie sur l'argument original, et la preuve Lean de Navier-Stokes ne correspondrait pas à la preuve rédigée. C'est un préprint, que personne n'a encore relu.

Le dépôt lui-même illustre le propos. La famille 130, sur la transformée de Fourier, porte un titre qui promet un résultat « pour tout n » ; la documentation Lean dit que le résultat est sous-séquentiel². La preuve compile. Elle prouve autre chose que le titre.

Villani, LeCun, Tao : qui dit quoi ?

En France, la réaction la plus forte est venue de Cédric Villani. Invité de France Inter le jeudi 8 octobre, le médaillé Fields y voit « certainement le changement le plus radical en mathématiques depuis au moins quatre siècles, peut-être même depuis 1 000 ans »⁸. Après avoir parcouru les résultats, il estime qu'il y a là « au moins une douzaine de médailles Fields », et qu'aucune université ne produit des mathématiques de haut niveau à ce rythme.

LeCun va dans le même sens avec un autre argument. Le 7 octobre, Florent Krzakala (EPFL) avait écrit sur X, en pastichant l'incipit de L'Étranger : « Aujourd'hui, une partie des mathématiques est morte, ou peut-être hier je ne sais pas »¹⁰. Un clin d'œil. LeCun lui répond le lendemain⁹ :

« Au contraire. C'est une nouvelle ère qui s'ouvre pour les mathématiques. Une ère où la démonstration formelle est largement automatisée et où l'accent sera reporté sur le développement de nouveaux concepts, nouvelles abstractions, nouvelles définitions, et nouvelles conjectures. L'invention du bateau a réduit l'importance de la nage, mais a permis la découverte de nouvelles terres. »

Villani mesure le choc par les résultats, LeCun par ce qu'il libère, et aucun des deux ne dit qui relit, ni à quel rythme.

L'AGMAI, groupe consultatif hébergé par l'Institute for Advanced Study (François Charles, Camillo De Lellis, Timothy Gowers, Martin Hairer, Edward Witten, entre autres), a précisé le 6 octobre que son rôle ne doit être lu ni comme un jugement sur l'impact des résultats ni comme un aval du processus, et qualifie la publication de « début, pas l'achèvement » de la compréhension humaine⁶. Parmi ses recommandations du 29 septembre : formaliser, déposer dans un lieu qu'aucun labo d'IA ne contrôle et, dans son préambule, cesser de tester des problèmes avancés sur des modèles propriétaires⁷. OpenAI en a suivi une partie : 42 % de résultats formalisés, mais des papiers hébergés sur son propre GitHub, et issus d'un test sur un modèle propriétaire.

Terence Tao, cité par Fortune, déplore des problèmes résolus par des prompteurs incapables de les exposer, et des pistes gardées secrètes par peur d'être devancé¹¹. Son blog accueille deux billets invités : la déclaration de l'Association for Human Mathematics, qui appelle à cesser de collaborer avec OpenAI¹⁴, et Hexagon, signé Ben Antieau, un dépôt communautaire qui accepte des soumissions entièrement générées par LLM¹⁵.

D'autres sont plus enthousiastes. Daniel Litt (Toronto) juge la publication excellente pour les mathématiques, tout en estimant, selon Fortune, qu'OpenAI n'emploie pas assez de mathématiciens spécialistes d'assez de domaines¹¹. Scott Aaronson, dans un billet titré « The Mathocalypse » (7 octobre), parle de « surely one of the biggest days in mathematical history », et rapporte que Dana Moshkovitz a trouvé l'article sur Unique Games impossible à lire sans l'aide d'une IA¹³. Dans Quanta, Dor Minzer (MIT) raconte avoir publié en septembre, avec deux étudiants, 95 pages sur une variante 4-to-1 pour ne pas être éclipsé, et Mark Braverman (Princeton) jugeait dès septembre, à propos des rumeurs, que les mathématiques par communiqué de presse ne sont pas saines¹².

Que fait-on quand la cuisine sort les plats plus vite qu'on ne goûte ?

Toute cuisine qui produit plus vite qu'on ne goûte finit par servir des plats que personne n'a mis en bouche. C'est la situation des 719 manuscrits : trois heures de calcul par résultat, des semaines d'expert pour le lire, parfois une poignée de spécialistes au monde capables de le faire. Lean ne dispense pas du goûteur. Quelqu'un doit prendre l'énoncé, le mâcher, et vérifier qu'il a bien le goût que le titre annonce ; la famille 130 et le signe faux des variétés abéliennes de dimension 8 montrent ce qui passe en cuisine quand personne ne le fait. Tout goûter prendra des années. Il faudra choisir ce que l'on goûte en premier.

Les mathématiques ont déjà connu ce décalage, à l'échelle d'un seul homme. En janvier 1831, Évariste Galois dépose à l'Académie des sciences le mémoire qui fonde ce qu'on appellera la théorie de Galois¹⁸²⁰. Le rapport, lu le 4 juillet 1831, signé Lacroix et Poisson (ce dernier l'a probablement rédigé), dit : « ses raisonnements ne sont ni assez clairs, ni assez développés pour que nous ayons pu juger de leur exactitude ». Le rapport refuse la publication en l'état, mais invite l'auteur à publier sa théorie en entier avant tout jugement définitif¹⁸²⁰. Poisson constate qu'il ne peut pas vérifier, et s'arrête là.

L'écart tenait aux concepts : Galois raisonnait sur des structures, les groupes de permutations, quand ses lecteurs attendaient des formules, et faute de vocabulaire partagé ses raccourcis passaient pour des trous. Dans la nuit du 29 au 30 mai 1832, veille de son duel, il note en marge d'un manuscrit : « Il y a quelque chose à compléter dans cette démonstration. Je n'ai pas le temps. »¹⁹ En 1843, Joseph Liouville annonce à l'Académie avoir trouvé dans les papiers de Galois une solution « aussi exacte que profonde », et la publie en 1846 dans son Journal²⁰. Quinze ans entre le rapport et la publication.

Le parallèle a ses limites : Galois était seul et inconnu, la machine d'OpenAI (modèle, harnais, contexte) produit à l'échelle industrielle, et Lean vérifie déjà 42 % des résultats principaux. La leçon tient quand même. Une démonstration n'existe qu'une fois comprise et transmise, et LeCun dit la même chose quand il place la valeur dans les concepts et les définitions. Galois a attendu quinze ans un lecteur qui parle sa langue ; des manuscrits signés par une machine, que Dana Moshkovitz ne lit pas sans IA, posent le même problème, multiplié par 719.

Ce que ça change pour l'entreprise

La structure du dépôt est la première leçon. Les fichiers « challenge » et les configurations Comparator séparent la spécification de l'implémentation, comme une suite de tests séparée du code qu'elle juge, et un tiers rejoue la vérification sans accès à la machine qui a généré la preuve⁴. Bastounis, Circelli et Hansen en montrent la limite, que connaît toute équipe qui a déjà eu des tests verts sur une mauvaise spécification : Lean garantit que la preuve prouve l'énoncé, et se tait sur le choix de l'énoncé⁵. Une seule configuration sur 405 avec le second noyau activé, c'est une CI dont un contrôle est désactivé par défaut⁴. Le retrait du 7 octobre dit le reste : trois manuscrits dépendaient d'un signe, et seule une relecture l'a vu³.

Pour le DSI, c'est la thèse de LeCun transposée. Quand la preuve, ou le code, s'automatise, la valeur humaine remonte vers la définition : poser l'énoncé, choisir l'abstraction, écrire la spécification que la machine devra satisfaire. Le goulot s'est déplacé : trois heures de calcul produisent un manuscrit, des semaines d'expert servent à le lire, et Villani constate qu'aucune université ne suit cette cadence⁸. Une équipe de revue de code sans outillage non plus : c'est l'effet miroir que DORA 2025 décrit pour le code, produit en quelques heures et relu en quelques jours.

Pour le CTO et le lead dev, le dépôt donne la recette d'une CI assez robuste pour absorber le débit des agents : une spécification exécutable relue par un humain (en logiciel, un modèle TLA+ ou une suite de tests de contrat joue le rôle du fichier challenge), plusieurs vérificateurs indépendants activés par défaut, et un changelog qui date chaque retrait. Le développeur qui passe de créateur à vérificateur a besoin de ces outils, sinon la fatigue décisionnelle fait le reste.

Pour le RSSI et les achats, le dénominateur reste flou. Le README parle d'environ 4 000 problèmes posés, Aaronson rapporte (« apparently », écrit-il) environ 8 000 et compte trois heures « par problème résolu », et Scientific American note que certains résultats ont pu demander plusieurs tentatives²¹³¹⁶. Personne ne sait si les tentatives échouées entrent dans la moyenne : demandez ce chiffre à tout fournisseur avant d'estimer le coût d'un résultat utilisable. Reste la confiance. Le modèle, le harnais d'agents, les prompts et les chaînes de raisonnement complètes restent fermés ; personne ne peut auditer une contamination éventuelle ni rejouer la génération. Ma règle : la confiance accordée à la sortie d'une machine IA (modèle, harnais, contexte) doit être proportionnelle à ce qu'un tiers peut vérifier sans cette machine.

Le point de vue SFEIR

La valeur se déplace de la génération vers la vérification, et le dépôt d'OpenAI l'a démontré en un jour. Les équipes qui investissent dans des spécifications exécutables relues par des humains, dans une revue outillée avec plusieurs contrôles indépendants activés par défaut, et dans un versionnage qui date chaque retrait, absorberont le débit des agents au lieu de le subir. Ce sont les trois chantiers sur lesquels SFEIR accompagne ses clients.

Sources

1. OpenAI, « Sharing AI progress in mathematics », billet du 6 octobre 2026 : openai.com ; version française (fr-CA) : openai.com/fr-CA.
2. Dépôt openai/math, README (722 manuscrits et 372 familles au commit initial du 6 octobre 2026 ; 719 manuscrits, 300 résultats principaux formalisés, exceptions à la procédure, famille 130, licence Apache 2.0) : github.com/openai/math.
3. Dépôt openai/math, fichier history.md (retrait de trois manuscrits le 7 octobre 2026, 14 révisions, 13 mises à jour de citations) : github.com/openai/math/blob/main/history.md.
4. Forum développeurs OpenAI, fil « First look at mathematics manuscripts from an internal frontier model at OpenAI » (recompilation de la famille 003 par davegoldblatt via Claude Code, 7 octobre 2026 01:52 UTC ; configurations Comparator ; extension ω ≤ 9/4 par selanavot avec Codex) : community.openai.com.
5. Alexander Bastounis, Fabian Circelli, Anders C. Hansen, « Navier-Stokes lost in translation: Why Lean verification of AI autoformalisation does not guarantee correct natural language proofs », arXiv:2610.08144 (v1, 6 octobre 2026, préprint non relu) : arxiv.org.
6. AGMAI, déclaration du 6 octobre 2026 (rôle du groupe, « le début, pas l'achèvement ») : agmai.org.
7. AGMAI, recommandations générales du 29 septembre 2026 (formalisation, dépôt hors du contrôle des labos d'IA, préambule sur les modèles propriétaires) : agmai.org.
8. franceinfo, Stéphane Jourdain, « "Le changement le plus radical en mathématiques depuis au moins quatre siècles" : Cédric Villani reconnaît les prouesses de l'intelligence artificielle » (France Inter, jeudi 8 octobre 2026) : franceinfo.fr.
9. Yann LeCun (@ylecun), réponse à Florent Krzakala sur X, 8 octobre 2026 (« Au contraire. C'est une nouvelle ère qui s'ouvre pour les mathématiques… ») : x.com.
10. Florent Krzakala (@KrzakalaF), message sur X, 7 octobre 2026 (pastiche de l'incipit de L'Étranger) : x.com.
11. Fortune, Jeremy Kahn, 7 octobre 2026 (réactions de Terence Tao via Mastodon et de Daniel Litt) : fortune.com.
12. Quanta Magazine, Ben Brubaker, « As AI Closed In on Unique Games Proof, Researchers Raced to Beat the Machines », 7 octobre 2026 (preuve Lean 2-to-1 sans édition humaine ; Dor Minzer, Mark Braverman ; total de 377) : quantamagazine.org.
13. Scott Aaronson, « The Mathocalypse », Shtetl-Optimized, 7 octobre 2026 (Dana Moshkovitz, estimation « apparently » d'environ 8 000 problèmes, trois heures par problème résolu) : scottaaronson.blog.
14. Blog de Terence Tao, billet invité : déclaration de l'Association for Human Mathematics sur la publication du 6 octobre, 7 octobre 2026 : terrytao.wordpress.com.
15. Blog de Terence Tao, billet invité signé Ben Antieau : « Hexagon », 6 octobre 2026 : terrytao.wordpress.com.
16. Scientific American, Joseph Howlett, « OpenAI Unleashes Hundreds More Math Results upon a Field Already in Shock », 6 octobre 2026 (un prompt, un agent ; essaim de 10 000 agents pour Navier-Stokes ; tentatives multiples) : scientificamerican.com.
17. ThePrint, Vrinda Tulsian, 7 octobre 2026 (les quatre résultats mis en avant par Sam Altman) : theprint.in.
18. BibNum, le mémoire de Galois de 1831 et le rapport de Lacroix et Poisson : journals.openedition.org/bibnum.
19. MacTutor History of Mathematics, « Évariste Galois » (note en marge de la nuit du 29 au 30 mai 1832) : mathshistory.st-andrews.ac.uk.
20. Wikipédia (fr), « Évariste Galois » (dépôt de janvier 1831, rapport du 4 juillet 1831, annonce de Liouville en 1843 et publication de 1846) : fr.wikipedia.org.