Maths : 722 preuves d’IA, 42 % seulement vérifiées

Le 6 octobre 2026, OpenAI a déposé sur GitHub 722 manuscrits de mathématiques écrits par un modèle interne que personne ne peut utiliser. Le lendemain, trois étaient retirés : une erreur de signe. Derrière la polémique, il y a une question que tu croises à chaque devoir : à partir de quand une démonstration est-elle vérifiée ?

En bref : le dépôt public openai/math contient 722 manuscrits regroupés en 372 familles de résultats, avec en moyenne trois heures de calcul de réflexion ChatGPT Pro par résultat. Le 7 octobre, trois ont été retirés après une erreur de signe qui en invalidait un et, par dépendance, deux autres ; il en reste 719. Le dépôt annonce 42 % de résultats principaux formalisés en Lean, mais l’expression n’est définie nulle part et des recomptes indépendants donnent plutôt 24 % ou 36 %. Pour toi, l’intérêt n’est pas la bagarre : c’est d’apprendre à séparer « ça a l’air juste » de « c’est vérifié ».

Ce qu’OpenAI a mis en ligne le 6 octobre 2026

Le dépôt openai/math contient des manuscrits en PDF, des formalisations en Lean et des résumés abrégés du raisonnement du modèle. Le README est explicite sur le coût : « On average, each result used three hours of ChatGPT Pro thinking compute with that model. »

Le modèle, lui, n’est pas accessible. Pas de nom public, pas de test possible, donc pas de reproduction possible : tu peux lire les preuves, tu ne peux pas rejouer l’expérience.

Le résultat le plus commenté porte sur l’hypothèse quasi-Riemann, un demi-plan sans zéro pour toutes les fonctions L de Dirichlet. Nature précise en revanche que le lot ne contient aucune solution aux cinq problèmes du millénaire encore ouverts.

Trois manuscrits retirés le lendemain : une erreur de signe

Le journal des modifications du dépôt date l’opération du 7 octobre 2026. Une erreur de signe invalide un argument de compensation dans « Algebraicity of Weil classes on split abelian eightfolds », déposé le 18 septembre. Deux autres manuscrits s’appuyaient sur cette construction : ils tombent avec lui.

Retraction Watch a détaillé l’affaire le 8 octobre : trois manuscrits retirés, quatorze révisés, treize mis à jour pour citer les versions corrigées. Un porte-parole d’OpenAI y dit accueillir favorablement l’examen critique de la communauté et s’engage à corriger vite. Andrew Sutherland, du MIT, lui répond dans le même article : les retraits seront vus positivement, « mais il faudra beaucoup plus que ça pour regagner la confiance perdue ».

Retiens la mécanique, elle est universelle : une erreur de signe, la faute la plus ordinaire qui soit, en bas d’une chaîne de dépendances, et trois travaux s’effondrent d’un coup.

42 %, 24 % ou 36 % : ce que « formalisé en Lean » veut dire

Lean est un assistant de preuve : un logiciel qui vérifie qu’une démonstration formelle découle bien d’un énoncé formel, via un petit noyau de confiance. Sur ce terrain, il est impitoyable. Le mathématicien Kevin Buzzard, cité par Matt Baker (Georgia Tech), le résume d’une phrase : « You cannot fool Lean; one learns this very early on. Lean will not accept proof by authority or proof by intimidation. »

Mais une formalisation ne garantit qu’une chose : que la preuve formelle correspond à l’énoncé formel. Elle ne garantit pas que cet énoncé dit la même chose que la phrase écrite en anglais dans le manuscrit. C’est l’écart de fidélité : un travail publié sur arXiv en juin 2026 rappelle qu’un énoncé formel « peut compiler et être démontrable tout en encodant un autre théorème que celui voulu par la source ». Prends « toute fonction continue sur un compact atteint son maximum » : plusieurs traductions en Lean compilent, mais celle qui oublie l’hypothèse d’ensemble non vide devient fausse sur l’ensemble vide. Matt Baker, lui, estime ce risque inférieur à 1 %.

Reste le chiffre. Le README annonce « ~42% top-line results formalized », soit 300 sur 719. Une analyse publiée par Pebblous montre que trois mesures circulent : 173 manuscrits sur 719 au catalogue de formalisation, soit 24 % ; 135 familles de résultats sur 372, soit 36 % ; et les 42 %, dont le numérateur de 300 « ne correspond à la longueur d’aucune liste du dépôt », l’expression « top-line results » n’étant définie nulle part. Cette phrase chiffrée est apparue deux jours après la publication, en remplacement d’un « Many, but not all, of the manuscripts have been formalized » beaucoup plus vague.

Autrement dit, même le taux de vérification demande à être vérifié.

La réponse des mathématiciens : l’AHM, puis Sophie Huiberts

Dès le 7 octobre, le groupe de travail Communications de l’Association for Human Mathematics a publié une déclaration, republiée le jour même sur le blog « What’s new » de Terence Tao. Sa formule la plus citée : « Releasing over 700 files at once is not a demonstration of scholarship, but a demonstration of power. » L’AHM, fondée mi-septembre 2026, appelle les mathématiciens à cesser de travailler avec OpenAI.

La position est loin de faire l’unanimité : les commentaires sous le billet sont nettement divisés. Certains refusent le boycott en faisant valoir que publier des preuves complètes, que chacun peut contrôler, est la position la plus exposée qu’un auteur puisse prendre.

Le 12 octobre, Tao a publié sur le même blog un billet invité de la mathématicienne Sophie Huiberts, « This is normal bad work ». Sa charge est précise : OpenAI ne prend pas la peine d’attribuer correctement les idées, « salami-slice 372 results over 719 pdfs », publie des travaux qui contiennent des erreurs méritant rétractation, promet du code sans le fournir, et livre des démonstrations « fiendishly hard to parse ». Détail qui en dit long : certains résultats avaient déjà été trouvés par des utilisateurs de ChatGPT en train de les rédiger proprement, à qui la publication en masse retire la paternité de leur travail. Sa thèse tient dans le titre : pas un cataclysme épistémique, du mauvais travail ordinaire publié sans gêne.

Septembre 2026 : la tribune des 25 médaillés Fields

Le terrain était préparé. Le 11 septembre 2026, 25 médaillés Fields — dont Cédric Villani, Pierre-Louis Lions, Hugo Duminil-Copin, Pierre Deligne et Yu Deng — signaient dans Le Monde une tribune intitulée « A Severe Misalignment of AI in Mathematics ». D’après la RTBF, ils y écrivent que les annonces arrivent « dans la précipitation, sans laisser le temps nécessaire à une rédaction rigoureuse », et que « cela soulève de graves questions d’attribution et de plagiat ».

Leur argument de fond vaut aussi pour toi : résoudre un problème n’est qu’un moyen au service d’un but, comprendre. Produire des résultats en masse à un rythme effréné risque, écrivent-ils, de détruire un terrain fertile au lieu de faire naître des idées nouvelles.

Le choc est réel. Dans franceinfo, le 12 octobre, Hugo Duminil-Copin, médaille Fields 2022, parle d’un « choc monumental » et dit : « J’en ai même pleuré. » Cédric Villani y voit « certainement le changement le plus radical en mathématiques depuis au moins quatre siècles ». Ursula Martin, d’Oxford, résume pour Nature le reproche pratique : cette publication revient à jeter à la communauté un premier jet mal tenu en attendant qu’elle fasse le ménage.

Ce que ça change pour toi

Tu ne vas pas relire une preuve sur les fonctions L de Dirichlet ce semestre. Mais cinq réflexes se transposent directement.

Une démonstration qui a l’air juste peut tomber sur un signe. Ce qui a coulé trois manuscrits d’OpenAI n’est pas un concept exotique, c’est une erreur de signe. Quand une IA te sort une solution bien rédigée, la bonne question n’est pas « est-ce que ça a l’air correct ? » mais « est-ce que je peux refaire chaque passage ligne à ligne ? ».

Les erreurs se propagent. Deux preuves sont tombées parce qu’elles dépendaient de la première. Si tu construis ton mémoire sur un résultat que tu n’as pas contrôlé, tu hérites de ses bugs.

« Vérifié » n’est pas un mot, c’est une question. Vérifié par quoi, contre quoi, sur quelle part du travail ? Entre 42 %, 36 % et 24 %, l’écart ne vient pas d’un mensonge mais de trois définitions du numérateur et du dénominateur. Devant n’importe quel pourcentage, demande-toi ce qu’on compte.

Un preprint n’est pas un article relu par les pairs. Les 719 documents n’ont été évalués par personne avant publication. Tu peux les citer, en disant ce qu’ils sont. Même règle pour les preprints arXiv, HAL ou SSRN de ta bibliographie.

L’attribution, c’est tout le sujet. Le reproche central fait à OpenAI est de ne pas citer les travaux antérieurs — exactement ce qu’on te demande dans un mémoire. C’est ce qui distingue une contribution d’un dépôt de fichiers.

Dernier réflexe, quel que soit l’outil : vérifie les règles d’usage de l’IA de ton établissement avant de t’appuyer dessus pour un travail noté, et déclare honnêtement ce que tu as utilisé.

Notre lecture

Les deux camps ont raison sur des choses différentes, et c’est ce qui rend le débat confus.

Sur le fond mathématique, quelque chose d’important s’est produit. Matt Baker, qui qualifie pourtant la publication de bâclée, parle d’un « tournant dans l’histoire des mathématiques ». Ignorer ça par principe serait une erreur.

Sur la méthode, les critiques sont solides, et elles ne portent même pas sur l’IA. Ne pas citer, découper un résultat en tranches, promettre du code absent, publier 722 documents que personne n’a relus : ce sont des fautes de métier qu’on reprocherait à n’importe quel auteur humain.

Ce qui nous frappe le plus, c’est le chiffre de 42 % : ajouté deux jours après la publication, avec un numérateur qui ne correspond à aucune liste du dépôt, et repris tel quel par toute la presse. Une affaire qui parle de vérification mathématique, et dont le chiffre clé n’est lui-même pas vérifiable.

Pour toi, la conclusion est simple et un peu rassurante. La valeur n’est plus dans la production d’une réponse : une machine le fait en trois heures de calcul. Elle est dans la capacité à relire, à repérer une erreur de signe, à dire d’où vient une idée et à expliquer pourquoi c’est vrai. C’est exactement ce que tes examens évaluent.

FAQ

OpenAI a-t-il résolu l’hypothèse de Riemann ?

Non. Le résultat le plus commenté porte sur l’hypothèse quasi-Riemann, un énoncé plus faible. Nature précise que le lot du 6 octobre ne contient aucune solution aux cinq problèmes du millénaire encore ouverts.

Puis-je citer un de ces manuscrits dans mon mémoire ?

Oui, à condition de dire ce que c’est : des preprints non relus par les pairs, produits par un modèle d’IA non public, dont certains ont été retirés ou corrigés. Cite la version et sa date, et signale le statut du document.

Qu’est-ce que Lean, concrètement ?

Un assistant de preuve : un logiciel qui vérifie mécaniquement qu’une démonstration formelle découle d’un énoncé formel. Très fiable sur ce point précis, mais il ne vérifie pas que l’énoncé formel traduit fidèlement la phrase écrite en langue naturelle dans l’article.

Pourquoi les chiffres varient-ils entre 24 % et 42 % ?

Parce qu’on ne compte pas la même chose : 173 manuscrits sur 719 au catalogue de formalisation donnent 24 %, 135 familles sur 372 donnent 36 %, et les 42 % d’OpenAI portent sur des « résultats principaux » que le dépôt ne définit pas.

Est-ce que ça veut dire que l’IA est mauvaise en maths ?

Non, et c’est plutôt l’inverse qui inquiète les mathématiciens. Le reproche ne porte pas sur le niveau des résultats, mais sur la façon de les publier : sans attribution, sans relecture, sans code.

Pour aller plus loin

• IA et intégrité académique : ce que disent vraiment les universités
• Citer une source en APA 7, ISO 690 ou Vancouver
• Réviser avec l’IA sans tricher : rappel actif, Feynman, quiz
• /skills/resume-article-scientifique