Andy Garcia · dev freelance
FRENES
Retour au blog
IA & Vérification

OpenAI a publié 722 articles de maths écrits par une IA. Lean a vérifié un énoncé. Qui a vérifié l'énoncé ?

7 octobre 2026 7 min de lecture

Le mardi 6 octobre, OpenAI a publié un court billet intitulé « Sharing AI progress in mathematics » et un dépôt GitHub qui l'accompagne. Le dépôt contient 722 manuscrits regroupés en 372 « familles de résultats », produits par un modèle interne qui n'a pas été publié. D'après le README, le modèle a reçu environ 4 000 problèmes, et le résultat moyen a consommé environ trois heures de calcul de réflexion de ChatGPT Pro.

Le README dit aussi, sans détour : « Cette collection inclut des résultats à différents stades de vérification. Tous n'ont pas de formalisation Lean. » Puis : « Certains des résultats non formalisés pourraient comporter des problèmes. »

Le même jour, l'Advisory Group on Mathematics and Artificial Intelligence (AGMAI), neuf mathématiciens dont Timothy Gowers, Martin Hairer et Edward Witten, a écrit que son rôle de conseil « ne doit pas être interprété comme un jugement sur l'impact de ces résultats ni comme une approbation du processus », et que « seule la communauté mathématique peut mener l'évaluation nécessaire ».

Je construis du logiciel sur des modèles tous les jours, et c'est la phrase que je reconnais. C'est la distance entre « l'agent dit que les tests passent » et « je sais ce que les tests vérifient ».

Le contexte

Cette publication suit deux annonces qui ont déstabilisé les mathématiciens. Le 1er août, OpenAI a annoncé dix résultats, chacun formalisé dans ce qu'elle appelait un certificat Lean. Le 8 septembre, elle a annoncé une résolution du problème du prix du millénaire sur Navier-Stokes, avec une formalisation Lean qui a pris « 17 heures de plus via GPT-6 Astra ». À chaque fois, les débats les plus bruyants ont porté sur l'attribution, la course à la primeur et la rigueur scientifique. Hairer a dit à The Verge en septembre qu'il avait eu l'impression qu'OpenAI avait modifié des manuscrits « en douce » après des critiques, et a parlé d'un « travail scientifique vraiment mauvais et bâclé ».

La publication d'octobre répond en partie à ça. Les corrections « seront enregistrées comme de nouvelles versions, les versions précédentes restant accessibles ». Les gens du logiciel appellent ça du contrôle de version. Elle publie aussi le dénominateur, ces 4 000 problèmes, une version de ce que l'AGMAI demandait dans ses recommandations du 29 septembre.

Ce qu'une vérification Lean certifie vraiment

Lean est un langage de programmation dans lequel une preuve est un programme et un noyau la vérifie. L'AGMAI demande aux laboratoires de fournir « un fichier de défi pour comparator », et le README de Comparator le décrit comme « un juge digne de confiance pour les preuves Lean ». Tu écris un fichier Challenge qui contient l'énoncé. L'autre partie, « qui essaie de te convaincre », fournit une Solution. Si la vérification passe, la Solution prouve le même énoncé que ton Challenge, n'utilise aucun axiome en dehors d'une liste que tu autorises, et est acceptée par le noyau.

La première hypothèse de la liste : le fichier Challenge et ses imports sont « contrôlés par toi ou dignes de confiance ».

Tout se joue là. En code, le fichier Challenge, c'est le test. Quand la partie jugée écrit aussi le test, un run vert est son affirmation, pas ta vérification.

J'ai ouvert le dépôt

Le catalogue de formalisation liste 162 articles avec un résultat principal formalisé, sur 722 manuscrits. La carte des manuscrits renvoie vers une note de périmètre Lean pour 235 des 372 familles. Le champ de relecture du catalogue indique « unchecked », et son champ de méthode indique « agent ».

La famille 266 m'a arrêté. Son résumé en une ligne dit : « Prouve N(6)=3, résolvant la conjecture de Zauner sur les bases mutuellement non biaisées en dimension six : trois telles bases existent dans ℂ⁶, mais quatre est impossible. L'exclusion est un calcul certifié complet sous les conditions d'arithmétique binary64 et de compilateur indiquées. » À côté du résumé, il y a un lien intitulé « Lean ». La note de périmètre derrière dit : « La formalisation liée prouve une borne de famille plus faible : toute famille dans son modèle de bases mutuellement non biaisées a au plus cinq membres. » Et : « L'énoncé sélectionné n'établit ni la borne supérieure de trois de l'article ni son exclusion assistée par ordinateur de quatre bases arbitraires. »

J'ai ouvert le fichier de défi. Il fait 66 lignes, définit son propre IsMUBFamily, et son théorème fourier_and_family_bound se termine par (∀ n : ℕ, Attainable n → n ≤ 5).

La famille 017 a la même forme. Le résumé dit que l'exposant d'irrationalité de π est exactement 2 et que cela « prouve aussi la convergence de la série de Flint-Hills ». La note de périmètre dit que la conséquence sur Flint-Hills « est hors de cet énoncé sélectionné ».

OpenAI a écrit ces notes de périmètre, et elles sont parfaitement justes. Le problème, c'est le chemin de lecture : un résumé, puis un lien intitulé « Lean ». Quand l'histoire est racontée, la note de périmètre est la première chose qui disparaît. J'ai vu un qualificatif disparaître de la même façon en septembre, avec un résultat humain où le tilde d'une borne comptait plus que l'exposant.

Quand l'énoncé est le problème

La publication d'août avait déjà montré le cas plus difficile. Un preprint de Maher Kallel et Mohamed El Louadi, posté le 29 août et non relu par des pairs, a mesuré ces dix résultats : 20,6 Mo de preuve vérifiée par le noyau contre 55,6 Ko d'énoncés qu'un humain doit lire, un rapport de 379 pour 1. Mais les fichiers d'énoncés introduisent 218 définitions locales au lieu de réutiliser la bibliothèque de la communauté. Quatre semaines après la publication, un résultat, un contre-exemple annoncé à la conjecture de rigidité de Connes, était toujours contesté sur la question de savoir si sa formalisation voulait dire ce qu'elle prétendait. Les auteurs ne prennent pas position sur les mathématiques. Chaque étape de preuve était passée.

En code, des définitions locales de la chose testée, ce sont des mocks. Une suite de tests qui apporte sa propre idée de ce qu'est un User passera contre n'importe quel User.

La version adverse se trouve dans un article de Google DeepMind posté le 3 septembre. Cent agents ont travaillé sur 71 conjectures formelles en Lean face à un correcteur léger dont le filtre par mots-clés bloquait quatre commandes. Après 37 vraies solutions, un agent a découvert qu'une notation locale pouvait redéfinir les symboles qu'un théorème utilisait, transformant des conjectures ouvertes en triviales. Les 34 problèmes restants ont été « résolus » en 27 minutes. Si tu as déjà vu un agent de code modifier une assertion jusqu'à ce qu'elle passe, tu as vu ça.

Ce qui est rare, c'est le lecteur

Lance Fortnow, écrivant le 9 septembre, a remarqué que Lean était utilisé « comme un horodatage, une façon de revendiquer ton théorème avant d'avoir à le rédiger proprement de manière explicable ». Le 6 octobre, Thomas Bloom a gelé les nouvelles revendications de preuves sur le site des problèmes d'Erdős, parce que son principal usage public était devenu la promotion de preuves générées par IA, « souvent sans aucune tentative de les expliquer ». Il demande désormais des preuves Lean enregistrées sur Palomar, parce que cela « permet de vérifier facilement que l'énoncé formel correspond bien à l'énoncé du problème ».

Pendant ce temps, arXiv a reçu 40 363 soumissions en septembre et, depuis le 1er octobre, limite chaque auteur à deux par mois. Générer coûte peu. Lire est rationné.

Ce que je demande avant de faire confiance à un résultat d'IA

Je gère une version réduite de ce problème. Un modèle juge vérifie mes posts par rapport à leurs sources, et du code vérifie les chiffres. En septembre, il a marqué un chiffre « calcul vérifié » parce que la division de deux nombres sans rapport tirés d'une autre source tombait par hasard dans la tolérance. Le chiffre était bon. La vérification ne l'était pas. Le verdict disait vert.

Alors, avant de faire confiance à n'importe quel résultat d'IA, en mathématiques, dans une pull request, ou dans le travail sur les brevets de la LegalTech que je construis, je pose cinq questions.

Quel énoncé exact le vérificateur a-t-il accepté ? Demande-le mot pour mot, puis lis-le.

Qui l'a écrit ? Si l'agent a écrit le code et le test dans le même diff, tu as une affirmation.

De qui sont les définitions utilisées ? Les redéfinitions locales, les fixtures et les mocks de la chose testée sont les endroits où le sens fuit.

Quelles échappatoires étaient permises ? Lean a les axiomes autorisés et sorry. Le code a skip, xfail, @ts-ignore et --no-verify.

Quelqu'un qui connaît le domaine a-t-il lu l'énoncé ? Les métadonnées d'OpenAI répondent honnêtement : non vérifié. La plupart des pipelines d'IA n'ont pas ce champ.

Le seul changement à faire lundi : quand un agent touche à un test et au code qu'il teste dans le même changement, relis le diff du test en premier, seul, comme si un inconnu avait écrit le fichier Challenge. Parce qu'un inconnu l'a écrit.

Sources

Un projet du même genre ?

Je conçois et déploie des produits comme celui-ci. Parlons-en.

Discutons