- Des modèles des familles ChatGPT et Claude ont produit en quelques semaines des contre-exemples à la conjecture des distances unitaires d’Erdős, à une question de Grothendieck sur les schémas en groupes et à la Jacobian Conjecture ; certains ont été vérifiés avec Lean
- Sol d’OpenAI a formalisé en trois semaines, en 1,2 million de lignes de code Lean, le contre-exemple d’Erdős ainsi que les résultats nécessaires de théorie globale des corps de classes ; c’est plus de la moitié des 2,3 millions de lignes de mathlib écrites en neuf ans
- Pour la question vieille de 60 ans de Grothendieck, Sol a trouvé un contre-exemple de 12 pages et Fable l’a formalisé en 1 076 lignes en 4 heures, confirmant l’existence d’un schéma en groupes d’ordre 4 qui n’est pas annulé par 4
- La formalisation automatique accélère aussi fortement la recherche : Andrew Yang a écrit environ 250 000 lignes de code Lean en près de deux semaines, achevant de fait un projet sur le théorème de relèvement de modularité nécessaire au dernier théorème de Fermat
- Les mathématiques informelles générées par l’IA ne peuvent pas être prises pour argent comptant, mais si une conjecture est traduite en un énoncé Lean précis, preuves et réfutations peuvent être vérifiées mécaniquement ; les humains doivent alors tirer des contre-exemples une intuition mathématique plus profonde
La conjecture des distances unitaires d’Erdős et la théorie globale des corps de classes
- Le 20 mai 2026, ChatGPT a réfuté la conjecture des distances unitaires d’Erdős en géométrie discrète
- Il a construit un contre-exemple à l’aide d’un profond théorème de théorie des nombres de Golod et Shafarevich datant des années 1960
- Plusieurs mathématiciens avaient relu l’argumentation à l’avance et l’avaient jugée valide, mais il n’existait pas encore de formalisation Lean au moment de l’annonce
- Le 26 mai, Mike Freedman, médaillé Fields et directeur scientifique de Logical Intelligence, a annoncé que son système avait automatiquement formalisé dans Lean l’intégralité de l’article de ChatGPT
- La partie formalisée était l’énoncé selon lequel le théorème de Golod–Shafarevich implique le contre-exemple à Erdős
- Le théorème de théorie des nombres sous-jacent lui-même nécessite plus de 100 pages et s’appuie sur une vaste partie de la théorie globale des corps de classes
- Après l’école d’été de 2025 sur la formalisation de la théorie des corps de classes, le cas local avait été presque achevé en un an, mais le cas global restait ouvert
La formalisation complète de 1,2 million de lignes créée par Sol
- Le 26 juin, Boris Alexeev d’OpenAI a annoncé sur Lean Zulip avoir guidé le nouveau modèle Sol pour produire une formalisation complète du contre-exemple d’Erdős ne supposant rien d’autre que les axiomes mathématiques
- Sol a généré 1,2 million de lignes de code Lean en trois semaines
- mathlib, écrite sur neuf ans, compte 2,3 millions de lignes
- La qualité du code était inégale, mais il démontrait réellement des résultats difficiles de théorie globale des corps de classes et des théorèmes non triviaux sur la cohomologie des corps de nombres
- Lean étant un langage de programmation capable d’exécuter des commandes arbitraires, le code généré a été exécuté dans une sandbox afin de tenir compte du risque de code malveillant
- Cette échelle et cette vitesse ont conduit à considérer comme inévitable le développement massif de mathématiques générées par l’IA
Atelier Formalizing Fermat et accessibilité des outils
- L’atelier Formalizing Fermat, organisé du 6 au 10 juillet, a réuni 25 personnes, mais le système de formalisation automatique du sponsor Logos Research ne pouvait être utilisé que par 5 personnes simultanément
- Tous les participants ont reçu un abonnement Claude Max d’un mois afin de pouvoir utiliser Claude Fable, et OpenAI a également offert gratuitement un mois d’accès à ChatGPT Pro
- Sol devait sortir le 9 juillet
- Fable devait prendre fin le 7 juillet, mais l’accès a en réalité été maintenu
- Les participants ont pu utiliser Sol et Fable pendant 4 des 5 jours de l’atelier, et les outils de Logos pendant toute la durée
- Pour développer la théorie des schémas en groupes finis et plats nécessaire à la formalisation du dernier théorème de Fermat, des articles classiques ont été fournis à Fable et ChatGPT afin qu’ils rédigent des explications en langage naturel
- Logos a détecté qu’un énoncé figurant dans ces explications était faux et a produit un contre-exemple explicite
- Après vérification, le document généré par le LLM décrivant une construction standard était erroné, et les humains n’avaient pas repéré l’erreur à la lecture
- La différence est qu’au lieu de simplement répondre qu’il ne comprenait pas l’argument, il a fourni une preuve que l’argument était faux
La question de Grothendieck sur les schémas en groupes
- Akhil Mathew, professeur à l’Université de Chicago, a soumis à l’IA une ancienne question de Grothendieck demandant si tout schéma en groupes fini libre d’ordre (n) est annulé par (n)
- Deligne a prouvé le cas commutatif
- Grothendieck a prouvé le cas où l’espace de base est réduit
- Rene Schoof a traité davantage de cas, et Emiliano Torti a aussi prouvé un cas plus général dans un article paru l’année précédente
- Le 11 juillet, au lendemain de l’atelier, Sol a trouvé un contre-exemple et généré un PDF de 12 pages
- Lorsqu’une formalisation Lean complète a été demandée au lieu d’un résultat informel, Fable l’a automatiquement formalisée en 1 076 lignes en 4 heures
- Le fichier Lean a d’abord été inspecté pour vérifier qu’il ne contenait que des théorèmes et aucune commande de type suppression de fichiers, puis compilé sur un ordinateur portable
- Vérification que l’énoncé n’utilisait que des concepts de mathlib
- Vérification que l’énoncé exprimait bien l’existence d’un contre-exemple
- Vérification que la preuve compilait correctement
- La vérification complète a pris moins de 5 minutes
- La vérification a confirmé l’existence d’un schéma en groupes d’ordre 4 qui n’est pas annulé par 4
- Akhil Mathew a soumis ce contre-exemple sous forme de PR mathlib
- Le contre-exemple d’Erdős comptait environ 1 million de lignes, tandis que celui de Grothendieck n’en comptait qu’environ 1 000 et était bien plus simple, mais il s’agit d’un cas où une machine a résolu une question de géométrie algébrique vieille de 60 ans
Réactions d’experts et théorème de relèvement de modularité
- Le 14 juillet, un professeur de l’Imperial College a estimé que le fait que le contre-exemple à Grothendieck ait été trouvé si facilement montrait seulement que les humains n’avaient pas réfléchi assez longtemps au problème
- Le doctorant Andrew Yang a utilisé Sol et Fable pour formaliser dans Lean le théorème de relèvement de modularité, important pour le dernier théorème de Fermat
- Il a écrit 250 000 lignes de code Lean en près de deux semaines
- Cela lui a permis d’achever de fait le projet
- Un autre professeur de l’Imperial College trouvait difficile à comprendre que des doctorants paient 200 dollars par mois pour Sol et Fable, mais après avoir constaté ce résultat, il a jugé au contraire qu’un doctorant qui ne dépensait pas 200 dollars par mois pour ces outils était irrationnel
- Harvard offrait déjà un accès gratuit à Fable à tous ses doctorants, postdoctorants et professeurs
Contre-exemple à la Jacobian Conjecture
- Akhil Mathew et Levent Alpöge ont discuté de la recherche de contre-exemples supplémentaires en géométrie algébrique, et Fable a trouvé un contre-exemple à la Jacobian Conjecture, célèbre problème ouvert depuis environ 100 ans
- Levent Alpöge a publié sur X le résultat apparemment résolu pendant la finale de la Coupe du monde 2026
- Lorsque Akhil Mathew a proposé une nouvelle PR mathlib, Paul Lezeau avait déjà formalisé manuellement le contre-exemple et soumis une PR au dépôt Formal Conjectures de DeepMind
- mathlib ne contient pas de grande liste de conjectures mathématiques, mais le dépôt Formal Conjectures en possède une
- Une fois que les humains s’accordent sur un énoncé Lean qui capture fidèlement le sens d’une conjecture, il devient simple de vérifier si le code généré par l’IA prouve ou réfute cette conjecture
Ce qu’il reste aux humains après la vérification formelle
- Pour la Jacobian Conjecture, l’étape suivante consiste pour les humains à comprendre exactement ce qui se passe dans ce contre-exemple
- Pour le contre-exemple à Grothendieck également, un travail est en cours afin d’aller au-delà d’une simple liste de représentations et de calculs sur des anneaux arbitraires et d’en acquérir une compréhension plus profonde
- La valeur d’un contre-exemple ne se limite pas à clore formellement un problème ; elle s’accomplit dans le processus d’extraction d’intuitions qui permet aux humains de mieux comprendre les mathématiques
1 commentaires
Avis de Hacker News
Pendant mes années de doctorat, j’ai eu l’occasion de contribuer directement à un problème ouvert dans un cours de recherche de mon directeur. Un vendredi, le professeur a présenté une conjecture lisse et élégante qu’il espérait vraie, mais comme j’aimais les exceptions étranges et que je manquais aussi d’outils de preuve, je me suis concentré sur la recherche d’un contre-exemple et je l’ai trouvé en une heure.
Le professeur a passé tout le week-end à échouer à la démontrer ; cela a montré que, lorsque des personnes ayant des outils, attentes et motivations différents regardent le même problème, elles peuvent contribuer depuis des directions totalement différentes. Je n’étais pas comparable à mon grand directeur, mais à ce moment-là j’avais une raison de regarder ailleurs, et cela a mené à un petit contre-exemple, ma seule contribution à la recherche mathématique.
Cela dit, c’est peut-être parce que je travaille surtout sur des objets abstraits difficiles à comprendre ; pour les nombres ou les polynômes, l’inverse est très probable.
https://ima.org.uk/28009/sir-erik-christopher-zeeman-the-mat...
Yitang Zhang, célèbre pour la conjecture des nombres premiers jumeaux, a travaillé pendant sept ans sur la conjecture jacobienne à Purdue sous la direction de Tzuong-Tsieng Moh. Il s’est avéré que l’étape clé de sa thèse reposait sur un corollaire erroné de Moh ; Moh a refusé d’écrire une lettre de recommandation, et Zhang, incapable d’obtenir un poste dans l’enseignement ou la recherche, a fini par travailler plusieurs années chez Subway.
Je me demande ce qui se serait passé si ChatGPT avait existé lorsqu’il a commencé ses recherches en 1986. Aujourd’hui, c’est devenu une histoire de réussite émouvante, mais elle suscite des sentiments complexes, comme ce vers : « La vie de Yu Xin fut d’une désolation extrême, mais dans sa vieillesse, ses poèmes et ses fu ébranlèrent Jiangguan ».
En élargissant mes recherches vers les mathématiques, j’ai été surpris de voir qu’un grand nombre de propositions dans la littérature sont fausses et se sont largement propagées jusque dans la littérature appliquée. Même lorsqu’on signale un problème, la réaction est souvent la défense et le déni, comme dans l’anecdote de Zhang. Les LLM sont utiles pour les preuves, mais ils se trompent aussi lourdement ; ils ressemblent à une autre personne suggérant des pistes avec une intuition différente, donc je pense que le résultat aurait été le même en 1986.
En mathématiques, les contre-exemples sont très importants pour affiner les définitions et rendre les preuves plus précises. Je recommande le livre de 1976 d’Imre Lakatos, 《Proofs and Refutations》 ; il existe aussi un bon nombre de livres consacrés uniquement aux contre-exemples en topologie, probabilités, analyse, etc.
https://en.wikipedia.org/wiki/Proofs_and_Refutations
https://www.amazon.com/s?k=counterexamples
Trouver un contre-exemple évite de perdre du temps à démontrer une proposition fausse et permet de passer à un autre problème ; au moins en mathématiques, cela permet donc d’utiliser le temps de l’humanité de façon plus productive.
Tant que ce sont des humains qui jugent ce qu’est une preuve élégante et éclairante, il restera du travail aux mathématiciens humains.
Le fait que beaucoup de théorèmes en informatique portent sur des définitions inductives et coinductives aide aussi.
La version mathématique de 《La Ballade de John Henry》 sera sans doute écrite elle aussi par l’IA. Je me demande qui sera le dernier champion humain à produire une preuve « digne de figurer dans THE BOOK » que même une machine ne pourrait surpasser.
https://en.wikipedia.org/wiki/John_Henry_(folklore)
https://en.wikipedia.org/wiki/Proofs_from_THE_BOOK
Nous ne comprenons ni l’intérieur des capacités de l’IA ni leur courbe de croissance, et nous ne savons même pas avec certitude si ses performances sont volontairement sous-affichées. Ce pourrait être un phénomène émergent résistant à la mesure, ou devenir aussi prévisible qu’une horloge dans quelques années. Personne ne sait ; ceux qui savent ne le disent pas, et ceux qui parlent fort n’en savent rien.
Si cela accélère fortement l’obtention de résultats significatifs par les doctorants, il n’y a aucune raison de ne pas investir 2 400 $ par an et par étudiant. Rapporté au coût total, c’est presque une broutille.
À l’université, j’aurais aimé disposer d’une formalisation Lean produite par un LLM. Les maths dans les diapositives de cours comportaient beaucoup d’erreurs, et certains professeurs refusaient les demandes d’explication en disant que « la preuve est dans les slides », tout en étant peu enclins à reconnaître les erreurs.
Les preuves Lean elles-mêmes ne sont souvent pas adaptées à la compréhension, mais j’espère qu’on pourra générer à partir d’elles des raisonnements plus faciles à comprendre pour les humains.
Le dépôt Agda TypeTopology de Martín Escardó en est un bon exemple. À l’inverse, les formalisations actuellement générées par des LLM peuvent être très brouillonnes ; même si elles certifient une vérité et contiennent un raisonnement intéressant, il faut beaucoup de travail pour les polir sous une forme qui améliore la compréhension mathématique. Un tutoriel interactif d’Agda se trouve sur lets-play-agda.quasicoherent.io.
Je me demande si, pour les mathématiciens, les contre-exemples sont, comme les résultats inattendus en sciences physiques, quelque chose qui peut être agaçant sur le moment mais extrêmement important parce qu’ils révèlent l’inexactitude d’un modèle, ou bien s’ils relèvent plutôt du rapport de bug en programmation : un détail mineur et pénible.
Les mathématiciens ont tendance à garder en tête tout un zoo de contre-exemples. Lorsqu’ils reconstruisent un théorème, ils peuvent aussi penser à des contre-exemples frappants et mémorables, puis restreindre le domaine et les conditions de manière à les exclure.
Une bonne partie de ces mathématiques est difficile à comprendre, mais cela semble surtout concerner la démonstration de théorèmes. Si les mathématiques par IA continuent d’accélérer, je me demande si elles découvriront un jour de nouvelles mathématiques applicables à l’ingénierie ou à la biomédecine, si l’humanité est à la veille d’une percée majeure, ou si cela se limitera à prouver ce qui est déjà connu.
https://en.wikipedia.org/wiki/Compressed_sensing
Un jour, les mathématiciens pourraient être submergés par des preuves à examiner, et des propositions fausses mais défendues avec trop de confiance pourraient entrer dans la communauté mathématique. Les mathématiciens du futur finiront peut-être comme les ingénieurs logiciels qui utilisent l’IA, à inspecter des milliers de lignes de preuves générées par IA pour y trouver des erreurs subtiles.