L'IA surpasse les mathématiciens humains en contre-exemples
Original : Human mathematicians are being outcounterexampled
Pourquoi c'est important
L'IA peut désormais produire et formaliser des mathématiques avancées à une vitesse inédite.
En mai 2026, ChatGPT a réfuté la conjecture de distance unitaire d'Erdős. En juin, le modèle Sol d'OpenAI a produit une formalisation complète en Lean en 1,2 million de lignes de code en trois semaines, couvrant des théorèmes avancés de théorie des corps de classes.
Le 20 mai 2026, ChatGPT a réfuté la conjecture de distance unitaire d'Erdős en géométrie discrète, en s'appuyant sur un théorème de Golod et Shafarevich des années 1960. Des mathématiciens humains ayant eu accès anticipé ont confirmé la validité de l'argument. Dès le 26 mai, la société Logical Intelligence — cofondée par le lauréat du prix Turing Yann LeCun et dont le directeur scientifique est le médaillé Fields Mike Freedman — a annoncé avoir autoformalisé le papier dans le langage Lean. Kevin Buzzard (mainteneur de mathlib) et son post-doctorant Thomas Browning ont vérifié ce travail. Le 26 juin, Boris Alexeev (OpenAI) a publié une formalisation complète reposant uniquement sur les axiomes des mathématiques, générée par le modèle Sol en 1,2 million de lignes de code Lean en trois semaines. À titre de comparaison, mathlib — la bibliothèque de référence de Lean — compte 2,3 millions de lignes et a nécessité neuf ans de développement collaboratif. Buzzard note que cette formalisation couvre des théorèmes difficiles de théorie globale des corps de classes, domaine dont la formalisation semblait encore hors de portée en 2025.