722 manuscrits de maths produits par l’IA d’OpenAI, 162 seulement vérifiés par ordinateur

Le fait

Le dépôt range les 722 textes en 372 « familles » de résultats, réparties sur 17 disciplines. OpenAI dit avoir soumis environ 4 000 problèmes à son modèle. Chaque résultat a demandé en moyenne trois heures de calcul « ChatGPT Pro thinking ». Dix résumés abrégés du raisonnement de la machine sont joints. L’ensemble est publié sous licence Apache 2.0.

Les problèmes visés portent des noms célèbres. La famille 003 s’intitule « The quasi-Riemann hypothesis ». Elle affirme qu’aucune L-fonction de Dirichlet ne s’annule quand la partie réelle de la variable dépasse 7/8, la fonction zêta de Riemann comprise. L’hypothèse de Riemann, toujours ouverte, place ces zéros sur la droite où la partie réelle vaut 1/2. L’écart reste donc large. D’autres familles annoncent une réponse négative au dixième problème de Hilbert sur les rationnels, ou un exposant d’irrationalité de π égal à 2 (sommaire du dépôt).

La répartition par discipline montre un modèle généraliste. L’informatique théorique arrive en tête avec 40 familles. Suivent la combinatoire (37) et la géométrie algébrique et complexe (36).

Notre regard

Trois questions suffisent pour juger ce genre d’annonce, celle-ci comme la prochaine. La preuve est-elle contrôlée par une machine ? Le résultat est-il neuf ? Compte-t-il pour les spécialistes ?

Sur la première, le dépôt ne répond qu’en partie. Lean a validé 162 textes sur 722. Ce logiciel est un assistant de preuve. Les 560 autres manuscrits attendent une relecture humaine. OpenAI l’écrit en toutes lettres : « some of the unformalized results could have issues », autrement dit certains résultats non formalisés pourraient comporter des erreurs.

Lean a aussi ses limites : il certifie que la preuve démontre l’énoncé tel qu’il a été traduit en code. Si cette traduction s’écarte de l’énoncé du papier, la coche verte ne garantit plus rien. Un humain doit donc relire au moins l’énoncé.

Les deux autres questions relèvent des spécialistes et de l’évaluation par les pairs, qui prend des mois. Le volume complique la tâche : environ 4 000 problèmes ont été posés pour 372 familles publiées, soit à peu près un problème sur onze. Personne ne sait encore combien de ces familles résisteront à l’examen. Le tableau détaille les huit disciplines les plus fournies.

La nuance

Les premières réactions vont de l’enthousiasme à la prudence. Levent Alpöge travaille chez Anthropic, concurrent d’OpenAI. Il a salué les résultats sur les zéros des L-fonctions, propos rapportés par la lettre Latent Space.

« C’est évidemment le moment le plus important de l’histoire des mathématiques. »

Levent Alpöge, chercheur (Anthropic)

D’autres voix relayées par la même lettre s’attendent à ce que certains résultats ne tiennent pas. Le dépôt signale lui-même deux exceptions à sa procédure standard. Il s’agit de la zone sans zéro de la fonction zêta et d’une preuve de la conjecture de Hodge pour les variétés abéliennes CM. La rédaction du résultat au-delà de 11/12 a été « retouchée par des humains pour la lisibilité ».

La forme de la publication suit les conseils d’un groupe consultatif indépendant. Hébergé à l’Institute for Advanced Study de Princeton, il a été annoncé le 21 septembre 2026. Ses neuf mathématiciens ne sont pas payés. Deux sont rattachés à des institutions françaises : François Charles (ENS-PSL) et Timothy Gowers (Collège de France). Cinq le sont à des institutions américaines. Le groupe ne conseille pas OpenAI sur le rythme de ses travaux internes.

À surveiller

Des chercheurs utilisent déjà ces modèles comme coéquipiers. Le diagramme de Venn symétrique à 19 courbes a été déposé sur arXiv le 22 septembre 2026. Chris Dzoba l’a obtenu avec Claude et Codex.

Avec 722 manuscrits d’un coup, la relecture humaine devient le goulot d’étranglement. C’est la pénurie d’experts que prédit Po-Shen Loh, professeur à Carnegie Mellon. OpenAI promet d’ajouter les formalisations Lean à mesure qu’il les obtient. Chaque correction paraîtra comme une nouvelle version, et les versions antérieures resteront consultables.

Une preuve fausse retirée demain restera donc lisible, juste à côté de sa correction.