OpenAI balance 722 manuscrits de maths d'un coup. Les mathématiciens crient au slopocalypse

Le 6 octobre, OpenAI a mis en ligne 722 manuscrits mathématiques. Sans conférence de presse, sans fanfare. Un dépôt GitHub, point. Générés par un modèle secret, vérifiés pour un cinquième seulement. La communauté n'a pas mis longtemps à réagir : l'Association for Human Mathematics appelle ses membres à couper les ponts avec OpenAI, et Nature parle de « slopocalypse ». Bienvenue dans le nouveau monde de la science.

722 fichiers, zéro avertissement

Le 6 octobre 2026 à 21h47, un dépôt nommé openai/math apparaît sur GitHub. Dedans : 722 manuscrits mathématiques, environ 799 mégaoctets de PDF, de sources LaTeX et de preuves Lean. En moins de 48 heures, il récolte 9 500 étoiles et un millier de forks.

Personne n'a été prévenu. Pas de communiqué retentissant. Pas de conférence. Juste un dossier balancé en ligne, comme on vide un carton de vieux papiers sur le trottoir.

Le souci, c'est ce qu'il y a dedans. OpenAI revendique des avancées sur la quasi-hypothèse de Riemann, la conjecture des jeux uniques, la conjecture de Hodge, le problème du facteur de groupe libre. Des problèmes que des générations de mathématiciens ont attaqués pendant des décennies, parfois un siècle. Et là, ils débarquent en lot, comme des figurines Panini.

Le grand jeu des trois chiffres

Avant d'aller plus loin, il faut remettre les compteurs à zéro. La confusion est le meilleur allié de ce genre d'annonce.

OpenAI dit avoir soumis environ 4 000 problèmes à son modèle. Il en sort 722 manuscrits, regroupés en 372 « familles de résultats ». Ces trois chiffres ne mesurent pas la même chose. Diviser 722 par 4 000 ne donne ni un taux de réussite, ni un taux de résolution. Ce sont des unités différentes : des problèmes posés, des documents écrits, des regroupements thématiques.

Traduit autrement : quand on vous dit « 4 000 problèmes », on ne vous dit pas combien ont été résolus. Quand on vous dit « 722 manuscrits », on ne vous dit pas combien sont corrects. Le dépôt contient ce qu'OpenAI a jugé bon de publier, pas tout ce que la machine a produit. L'analyse de XenoSpectrum le rappelle noir sur blanc : ce sont des unités différentes.

Le chiffre qui compte : 162

Il y a un chiffre qui compte vraiment, et il est enterré au milieu du README. Sur 722 manuscrits, 162 disposent d'une preuve formelle complète en Lean. Soit environ 22 %. Les deux tiers restants, 487 documents, ne reposent que sur le jugement interne d'OpenAI.

Lean, c'est l'assistant de preuve qui vérifie chaque étape logique par machine. Une preuve Lean qui compile, c'est une chaîne de raisonnement sans trou. Pas de triche possible. Pas de « on suppose que ».

Le README le reconnaît avec une candeur rare pour un laboratoire de cette taille : certains résultats non formalisés « pourraient comporter des problèmes », et OpenAI s'efforcera « de corriger rapidement tout problème de ce type ».

Traduisons. OpenAI admet noir sur blanc que les deux tiers de sa production sont potentiellement faux, et que ce n'est pas grave, ils corrigeront plus tard. Dans n'importe quelle revue de mathématiques, cette phrase vaudrait un refus immédiat.

Et encore. Une preuve Lean garantit l'absence d'erreur logique dans la chaîne codée. Elle ne garantit pas que le théorème formalisé corresponde à l'énoncé qu'on croit avoir démontré. C'est le piège classique : formaliser une version trop étroite du problème, et prouver autre chose que ce qui était annoncé.

Ce que le modèle revendique

Le catalogue est impressionnant sur le papier. La quasi-hypothèse de Riemann, avec un seuil de partie réelle repoussé. La conjecture des jeux uniques, centrale en complexité algorithmique. La conjecture de Hodge rationnelle pour les variétés abéliennes à multiplication complexe. Le problème du facteur de groupe libre. Des résultats partiels sur Birch et Swinnerton-Dyer et sur Goldfeld. Sans oublier l'exposant d'irrationalité de π et les conjectures de Mahler.

À ce stade, un détail doit être dit clairement : aucun de ces grands résultats n'a été confirmé par des mathématiciens indépendants. Zéro. Le Clay Mathematics Institute, gardien des problèmes du millénaire, n'a d'ailleurs toujours pas validé la revendication Navier-Stokes du mois dernier.

OpenAI précise aussi que deux familles échappent à la procédure standard, et que certains manuscrits ont été « édités par des humains pour les rendre lisibles ». Autrement dit, l'étiquette « entièrement généré par IA » mérite des guillemets.