OpenAI publie 722 manuscrits de maths sans dire combien sont vérifiés

Un dépôt apparaît à 21 h 47

Le 6 octobre à 21 h 47 UTC, un dépôt appelé openai/math apparaît sur GitHub. Dedans, 722 manuscrits de mathématiques, tous produits par un modèle interne d'OpenAI que personne, à l'extérieur, ne peut utiliser. Quatorze minutes plus tard, le dernier fichier est poussé. Le lendemain, le dépôt dépasse les 8 500 étoiles.

La presse titre sur deux chiffres différents : The Decoder annonce 372 résultats, unite.ai 722. Les deux ont raison, le README les réconcilie en une ligne : « 722 manuscrits organisés en 372 familles ».

Une famille regroupe les papiers qui tournent autour d'un même résultat : son argument principal, ses conséquences, ses preuves alternatives. Compter les familles ou les papiers, c'est compter les coffrets ou les disques.

Le mot qui a pris la place du chiffre

Reste la question que ni 722 ni 372 n'abordent : combien de ces preuves une machine peut-elle contrôler ?

L'annonce d'OpenAI ne le dit pas. Elle partage en Lean les formalisations de « beaucoup » de ces preuves. Beaucoup. Le mot fait le travail d'un nombre.

Formaliser, c'est réécrire une preuve dans un langage où l'ordinateur n'accorde rien : pas d'intuition, pas de « on voit facilement que ». Si une étape manque, ça ne compile pas. D'où le poids de ce compte, seul chiffre du dépôt qui renseigne sur la solidité du lot.

Les deux reprises divisées sur 722 et 372 ont recopié ce « beaucoup » à l'identique, sans donner le moindre compte : la dispute portait sur le chiffre décoratif, pas sur celui qui tranche. Un site spécialisé est allé le chercher et l'a publié, en citant le fichier d'où il sort. Sauf que ce fichier ne dit pas tout.

On a déjà raconté ici ce que cette vérification pèse : le 8 septembre, c'est une preuve contrôlée en Lean qui empêchait de balayer l'annonce d'une question ouverte depuis 1934.

162, et pourquoi ce n'est pas 44 %

Un fichier répond : lean/formalization.yaml, en version 0.4, que son en-tête annonce comme le « catalogue des papiers à résultat principal formalisé ». Il contient 162 entrées, chacune pointant un manuscrit.

162 sur 722 manuscrits, soit 22 % au relevé du 7 octobre. La date compte : le fichier est versionné et OpenAI prévient qu'il continuera d'en ajouter.

Un ratio plus flatteur circule facilement : 162 sur 372 familles, soit 44 %. Il est faux, et pas de peu. Les 162 entrées désignent des papiers, pas des familles, et 23 familles en portent plusieurs : la famille 331 à elle seule compte 7 papiers formalisés. Mettre des papiers au numérateur et des familles au dénominateur, c'est diviser des pommes par des cageots.

Le compte par famille, on l'a fait : ces 162 papiers couvrent 127 familles sur 372, soit 34 % au même relevé.

Le catalogue officiel oublie des preuves

Mais le dépôt porte un second registre, qui ne raconte pas la même chose. Dans la carte des manuscrits, 235 familles sur 372 renvoient vers une fiche décrivant le périmètre de leur formalisation Lean, et le dossier qui les héberge en contient exactement 235. Le catalogue, lui, n'en couvre que 127.

Cent huit familles ont donc une fiche Lean sans figurer au catalogue des résultats formalisés. L'inverse ne se produit jamais.

Prenons la famille 005, l'irrationalité de la constante de Catalan. Sa fiche est sans ambiguïté : « la formalisation prouve que la constante de Catalan est irrationnelle. C'est l'assertion mathématique du titre du papier. » Le fichier Catalan.lean est bien là, et le mot « Catalan » n'apparaît nulle part dans formalization.yaml.

Douze de ces 108 fiches ont été ouvertes une par une. Les douze décrivent une formalisation du résultat principal, de l'exposant d'irrationalité de π à la conjecture des sommes de réciproques d'Erdős. Ce ne sont pas des brouillons.

162 est donc un plancher : le registre officiel est plus court que l'étagère qu'il prétend décrire.

« Formalisé » ne veut pas dire « vérifié »

Un dernier écart, en sens inverse. On lit déjà que 162 preuves auraient été « vérifiées par Lean ». Personne n'a publié de vérification.

Ce qu'OpenAI livre, ce sont 405 fichiers d'énoncés et la marche à suivre pour les contrôler soi-même. Le dépôt n'embarque aucune intégration continue : aucun contrôle ne tourne tout seul, et le README de la bibliothèque Lean prévient que tout compiler d'un coup peut échouer. OpenAI tend l'enveloppe scellée et le coupe-papier, sans dire ce qu'il y a dedans.

Nous non plus : on a compté des fichiers et lu les descriptions de périmètre d'OpenAI, on n'a compilé aucune preuve. Et ces 405 fichiers ne sont pas 405 résultats : une seule famille peut en réclamer quatre.

Sur les 560 manuscrits sans entrée au catalogue, OpenAI écrit une phrase que ses reprises n'ont pas gardée : « certains des résultats non formalisés pourraient avoir des problèmes ».

Les deux résultats qui sortent du lot

Le README précise la fabrication : environ 4 000 problèmes posés au modèle, à peu près trois heures de calcul par résultat, et un tri qui a laissé ce catalogue.

Deux résultats y échappent, et le document le dit noir sur blanc : la région sans zéro de la fonction zêta de Riemann et la conjecture de Hodge pour les variétés abéliennes CM sont des « exceptions à cette procédure fixe ». Pour la première, OpenAI ajoute que la rédaction a été relue et corrigée par un humain, pour la lisibilité. Les deux résultats les plus prestigieux du lot sont donc ceux dont la fabrication ressemble le moins au reste.

Le comité cité en renfort a publié le contraire d'une caution

OpenAI dit s'être appuyée, pour la forme de cette publication, sur les recommandations publiques d'un groupe consultatif indépendant sur les mathématiques et l'IA, hébergé à l'Institute for Advanced Study. Le même jour, ce groupe publiait son propre texte sur la sortie, qui commence par refuser d'être lu comme une approbation : « le rôle consultatif de l'AGMAI ne doit pas être interprété comme un jugement sur l'impact de ces résultats ni comme une approbation du processus par lequel OpenAI les a obtenus. »

Il ajoute que cette publication est « le début, et non l'achèvement » du travail d'appropriation, et que c'est à la communauté mathématique d'en juger. Il dit les discussions constructives et salue la volonté d'OpenAI de dialoguer.

Il y a plus net encore. Ses recommandations du 29 septembre, celles que l'annonce invoque, s'ouvrent sur une demande que la sortie ne satisfait pas : « nous ne cautionnons pas cette pratique, et nous leur demandons d'arrêter de tester des problèmes mathématiques avancés sur des modèles propriétaires. » Les 722 manuscrits sortent précisément d'un modèle interne non publié. OpenAI dit travailler à le diffuser.

Ses neuf membres ne sont pas rémunérés : ils ont créé cette structure autonome après qu'OpenAI a approché certains d'entre eux pour un comité maison. Timothy Gowers, médaillé Fields, et Edward Witten en font partie.

Ne pas confondre ce comité de neuf avec le texte signé par vingt-cinq médaillés Fields paru le 11 septembre, dont on a déjà parlé ici : celui-là ne nommait aucune entreprise et ne se prononçait pas sur la validité d'une preuve. Deux documents, deux portées, avec un seul homme dans les deux : Martin Hairer, médaillé Fields 2014, signataire de la déclaration et membre du comité. Ne pas contester n'est pas approuver, et être cité n'est pas cautionner.