OpenAI a publié 722 manuscrits mathématiques produits par un modèle interne non publié, présentant ce travail comme le résultat d'un processus reposant en grande partie sur un prompt unique soumis à un agent unique. Les articles sont organisés en 372 familles de résultats apparentés, mais les mathématiciens affirment que les affirmations ne peuvent être pleinement évaluées tant que le modèle, les prompts et des preuves supplémentaires ne sont pas rendus disponibles.

Cette publication intervient alors que les laboratoires d'IA utilisent de plus en plus les mathématiques comme terrain d'essai pour le raisonnement des modèles de pointe, et elle s'annonce comme un premier test de la manière dont la recherche générée par l'IA devrait être publiée, vérifiée et divulguée.

Un porte-parole d'OpenAI a déclaré que presque tout provenait d'un prompt unique remis à un unique agent d'IA, bien que certains résultats aient pu nécessiter plusieurs tentatives. L'entreprise a indiqué avoir soumis environ 4 000 problèmes au modèle et sélectionné les résultats qu'elle jugeait suffisamment importants pour être publiés.

Andrew Sutherland, mathématicien au MIT, a déclaré à Scientific American que l'affirmation d'une résolution en une seule fois devait être traitée avec prudence. « Tant qu'ils n'auront pas publié le modèle et que les gens ne pourront pas reproduire leurs résultats, je pense que toute affirmation concernant la résolution de problèmes en une seule fois par un agent unique doit être considérée comme non vérifiée », a déclaré Sutherland. « Nous devrions exiger des preuves. »

Le chiffre de 722 représente des manuscrits plutôt que des problèmes résolus. Une famille de résultats peut contenir un théorème principal accompagné d'arguments complémentaires, de conséquences ou de preuves alternatives. OpenAI a indiqué que le résultat moyen a utilisé l'équivalent d'environ trois heures de calcul de réflexion de ChatGPT Pro. Cela diffère de l'affirmation de l'entreprise concernant Navier-Stokes le mois dernier, qui impliquait 10 000 agents coordonnés travaillant pendant 88 heures.

OpenAI a publié des résumés de raisonnement abrégés pour 10 résultats. Cependant, un catalogue de formalisation dans le dépôt GitHub montre que seuls 162 des 722 manuscrits comprennent actuellement un résultat principal vérifié par ordinateur. Cela représente environ 22 % de l'ensemble et signifie que le résultat a été traduit en Lean, un logiciel qui vérifie mécaniquement chaque étape logique. Lean est devenu la norme de travail pour les preuves vérifiées par machine en mathématiques, c'est pourquoi les quelque 560 manuscrits encore non formalisés constituent la principale question ouverte de cette collection.

OpenAI a reconnu que tous manuscrits n'ont pas de formalisations Lean et a averti que « certains des résultats non formalisés pourraient présenter des défauts ». Une vérification Lean réussie confirme seulement que la preuve découle de l'énoncé tel qu'écrit en Lean. Elle n'établit pas que l'énoncé correspond au problème d'origine, ni que le résultat est nouveau ou important. Ces questions nécessitent encore l'examen de mathématiciens.

Des chercheurs ont déjà fait part de leurs préoccupations concernant le matériel et la manière dont il a été publié. Dmitry Rybin a écrit sur X :

I was trying to read the OpenAI proof that chromatic number of a plane is >= 6. But it is totally unbelievable alien math? Somehow the model found that any K-coloring <=> "weakly measurable" K-coloring, which seems out of nowhere 1/2 pic.twitter.com/W13ScT3nel — Dmitry Rybin (@DmitryRybin1) October 7, 2026

Keith Adler a écrit sur X :

The openai/math repo has Issues turned off and has never accepted a pull request. That's disappointing. If you publish 722 manuscripts and ask for Lean formalisations, you need somewhere for people to send them. I'm formalising OpenAI's Saxl's Conjecture proof in Lean 4 against… — Keith Adler (@keithadler) October 7, 2026

L'Institute for Advanced Study de Princeton, dans le New Jersey, a également interrogé les implications du travail mathématique généré par l'IA. « Il est désormais possible que l'IA produise des arguments mathématiques dans des situations où l'humain qui a déclenché le processus n'est pas en mesure de comprendre ces arguments, de les vérifier ou d'en assumer la responsabilité », a déclaré l'institut dans un communiqué. « Nous pensons que la compréhension humaine des mathématiques reste d'une importance primordiale. Comment, dans cette nouvelle ère, pouvons-nous œuvrer à un nouveau paradigme qui intègre la compréhension humaine des mathématiques comme partie intégrante d'une production scientifique responsable ? »

Le professeur Abhishek Saha a adopté une vision plus positive, écrivant : « C'est un très grand jour pour les mathématiques. » Il a indiqué que la plupart des résultats relevaient de catégories telles que « avancées exceptionnelles au sein d'un programme existant » et « percées surprenantes ». Selon son évaluation, la collection contient des problèmes intéressants, mais pas de résultats comparables aux problèmes du millénaire, les sept questions à un million de dollars de la Clay Mathematics Institute. Il a identifié l'hypothèse quasi-Riemann comme le seul des 722 résultats à atteindre ce niveau d'importance.

Saha a écrit sur X :

Some further thoughts on the 372 results released by OpenAI today, across 722 manuscripts. If I were to classify theorems that mathematicians prove and publish according to their groundbreaking nature, I would (very roughly) divide them into four categories: A) Non-breakthrough… — Abhishek Saha (@ObhishekSaha) October 7, 2026

La publication n'a pas non plus satisfait les recommandations émises par un groupe consultatif de l'Institute for Advanced Study le 29 septembre. Le groupe recommandait de divulguer le nom du modèle, les prompts, une chaîne de raisonnement résumée, le temps nécessaire et le coût de calcul pour chaque résultat. OpenAI a fourni des chiffres de calcul moyens et 10 résumés de raisonnement, mais pas les prompts. L'entreprise a déclaré continuer à travailler à une publication responsable du modèle.

Daniel Litt, mathématicien à l'Université de Toronto, a adopté la position inverse, faisant valoir qu'il n'y avait aucune raison de demander à OpenAI de garder secrètes les réponses à ces questions mathématiques.

Anthropic a emprunté une voie différente le mois dernier en publiant sur GitHub la totalité des 13 millions de lignes d'une preuve du dernier théorème Fermat vérifiée par Lean. Ce travail a formalisé un théorème publié par Andrew Wiles en 1995 plutôt que de présenter de nouveaux résultats mathématiques. Les deux publications illustrent une divergence dans les stratégies de divulgation au sein de l'industrie : d'un côté une preuve complète et vérifiée par machine d'un théorème connu, de l'autre un vaste lot de nouvelles affirmations avec une vérification formelle partielle.

OpenAI a indiqué qu'elle ajouterait des formalisations Lean dès qu'elles seraient disponibles. Pour l'instant, 162 des 722 manuscrits en comportent une. Le statut des autres dépend désormais de ce que les chercheurs disent le plus nécessaire : la publication du modèle, les prompts sous-jacents et des formalisations indépendantes des manuscrits restants.