Le 20 juillet 2026, Kevin Buzzard, professeur de mathématiques à l’Imperial College de Londres, a publié un billet de blog dont la franchise a secoué la profession : les mathématiciens humains sont en train d’être « dépassés par les contre-exemples ». En l’espace de deux mois, l’IA a réfuté trois conjectures vieilles de plusieurs décennies — dont l’une restée ouverte depuis près d’un siècle.
Buzzard lui-même raconte : « Il m’a fallu moins de cinq minutes pour vérifier un contre-exemple de géométrie algébrique qui tenait depuis 60 ans. J’ai téléchargé le code Lean sur mon portable, la compilation a réussi, et j’ai hoché la tête en me disant : oui, c’est bien un contre-exemple. »
Cinq minutes. Voilà la ligne de partage entre les mathématiques humaines et celles de l’IA. L’objet de cet article est de comprendre quand cette ligne a été tracée et ce qu’elle implique.
Le contre-exemple : une lame plus tranchante que la preuve
Commençons par un concept élémentaire. En mathématiques, prouver qu’une assertion est vraie est difficile — il faut produire un raisonnement rigoureux où chaque étape est irréprochable. Mais prouver qu’elle est fausse est comparativement « simple » : il suffit d’exhiber un contre-exemple — une construction concrète qui satisfait toutes les prémisses mais pas la conclusion.
Si quelqu’un affirme que « tous les cygnes sont blancs », inutile de recenser tous les cygnes de la planète : il suffit d’en trouver un seul noir.
Un contre-exemple peut suffire à anéantir une vie de recherche. C’est aussi pour cela qu’il a toujours joué un rôle créateur en mathématiques — il révèle les limites d’une théorie, force les mathématiciens à réexaminer leurs hypothèses, à affiner leurs définitions, à faire progresser la discipline. D’une certaine manière, le contre-exemple est le carburant du progrès mathématique.
L’IA est en train de porter cette « chasse au cygne noir » à une échelle vertigineuse.
Mai à juillet 2026 : le triplé de l’IA
Voici la chronologie des événements de ces trois mois.
Premier coup : la conjecture d’Erdős sur la distance unité (posée en 1946, réfutée le 20 mai 2026)
Ce problème de géométrie discrète, formulé par le légendaire Paul Erdős en 1946, a cédé devant une construction proposée par ChatGPT. La première réaction de Buzzard fut de demander : « L’avez-vous vérifiée dans Lean ? » Non. Mais moins d’une semaine plus tard, Mike Freedman — médaillé Fields devenu directeur scientifique de Logical Intelligence — annonçait par courriel que leur système avait automatiquement traduit la démonstration en code Lean.
Un mois après, Boris Alexeev (OpenAI) allait plus loin avec le nouveau modèle Sol : une formalisation complète du contre-exemple à partir des axiomes mathématiques. Sol a généré 1,2 million de lignes de code Lean pour ce travail.
Pour donner une idée : la bibliothèque mathlib, fruit de neuf ans de travail de la communauté Lean, totalise 2,3 millions de lignes. En trois semaines, l’IA a produit l’équivalent de plus de la moitié de ce que l’humanité avait accumulé en neuf ans. Buzzard résume : « Le développement mathématique généré à grande échelle par l’IA est désormais inévitable. »
Deuxième coup : le problème du groupe formel de Grothendieck (posé dans les années 1960, réfuté le 11 juillet 2026)
Grothendieck, l’un des plus grands mathématiciens du XXe siècle, avait demandé il y a soixante ans : un groupe formel libre fini d’ordre n est-il nécessairement tué par n ? Deligne avait prouvé le cas commutatif, Grothendieck lui-même le cas où l’anneau de base est réduit — mais la question complète restait ouverte.
Sol a trouvé un contre-exemple. La preuve tient en 1076 lignes de Lean. Buzzard l’a vérifiée en moins de cinq minutes. Il a suggéré au mathématicien Akhil Mathew de soumettre ce contre-exemple à la bibliothèque mathlib, avant de plaisanter : « Et si tu t’attaquais à la conjecture de Hodge, ensuite ? »
Troisième coup : la conjecture jacobienne (posée en 1939, réfutée le 19 juillet 2026)
Le plus retentissant. La conjecture jacobienne est un problème inverse sur les applications polynomiales : si le déterminant jacobien d’une application polynomiale est une constante non nulle, l’application est-elle nécessairement inversible ? Depuis 1939, cette question figure parmi les conjectures les plus séduisantes—et les plus coriaces—de la géométrie algébrique.
C’est Claude Fable, d’Anthropic, qui a trouvé le contre-exemple, pendant la finale de la Coupe du monde 2026. Dès le lendemain, Terence Tao — l’un des mathématiciens les plus respectés de notre époque — publiait un billet détaillé pour « digérer » la portée mathématique du contre-exemple.
Les calculs de Tao montrent qu’il s’agit d’une application polynomiale à trois variables, de degré maximal sept. Son déterminant jacobien vaut −2 — une constante non nulle — mais l’application envoie trois points d’entrée distincts vers la même sortie : elle n’est pas injective, donc pas inversible. Plus frappant encore : l’IA a utilisé 120 paramètres ajustables pour contrôler les 1329 coefficients qui auraient théoriquement pu apparaître dans le déterminant jacobien, de sorte que tous les termes non nuls s’annulent exactement. Pour reprendre les mots de Tao : « Cela ressemble à un prodige. »
Lean + LLM : l’union de la créativité et de la preuve formelle
Après ces récits, examinons la logique technique.
Lean est un « compilateur mathématique ». Vous rédigez une preuve en Lean, et chaque étape doit passer un contrôle de typage strict. Pas de « l’étape évidente est laissée au lecteur » — tout doit être explicité jusqu’au niveau atomique. Si le code compile, la preuve est mathématiquement correcte — sans aucune confiance humaine nécessaire.
Le LLM (grand modèle de langage) se charge de l’« invention », Lean du « verdict ». La faiblesse des LLM en mathématiques est leur tendance à halluciner — à produire un raisonnement qui a l’air plausible sans être correct. Lean résout ce problème à la racine : le LLM génère du code Lean, le compilateur le vérifie immédiatement. Si la compilation échoue, le LLM reçoit le message d’erreur et peut corriger le tir. Itération après itération, jusqu’à ce que le code compile — et là, le résultat mathématique produit par l’IA bénéficie d’une garantie de validité absolue.
En mars 2026, un article intitulé « Learning to Disprove » a systématisé cette méthodologie. L’intuition centrale : plutôt que de demander à un LLM de « prouver » une assertion (risque d’hallucination), mieux vaut lui demander de « trouver un contre-exemple » — car un contre-exemple qui compile dans Lean est irréfutable. Les auteurs ont adopté une stratégie de « mutation symbolique » : supprimer systématiquement certaines conditions dans des théorèmes existants pour générer des données d’entraînement, puis entraîner le LLM avec un système de récompenses multiples. Résultat : une amélioration de 49 % de la précision dans la génération de contre-exemples.
Voilà le fondement technique du « dépassement par les contre-exemples » : le LLM apporte la créativité, Lean apporte la preuve formelle, et le mathématicien humain devient spectateur — du moins pour l’étape de vérification.
Les « cinq phases du deuil » chez les mathématiciens
Buzzard rapporte avec franchise les réactions de son entourage. À l’heure du déjeuner à l’Imperial College, il entend un collègue dire : « Si les contre-exemples sont si faciles à trouver, c’est juste que les humains n’ont pas consacré assez de temps à ces problèmes. » Buzzard a souri jaune : lui-même avait passé une semaine entière sur l’un de ces problèmes jugés « pas assez importants ».
C’est le déni, classique.
Puis vient la négociation. Un professeur écrit, surpris : pourquoi des étudiants de thèse acceptent-ils de payer 200 dollars par mois pour un abonnement à Sol et Fable ? La réponse de Buzzard est cinglante : « Tout étudiant en thèse qui ne dépense pas ces 200 dollars est irrationnel. » L’université Harvard a déjà offert un accès gratuit à Fable à tous ses doctorants, postdoctorants et enseignants en mathématiques.
Qu’on l’accepte ou non, un fait est clair : en recherche mathématique, l’écart de capacité entre ceux qui maîtrisent les outils d’IA et ceux qui ne les maîtrisent pas se creuse de mois en mois.
La voie tracée par Terence Tao
Parmi toutes les réactions, celle de Terence Tao est sans doute la plus instructive. Il n’a pas remis en cause les limites de l’IA, ni engagé un débat philosophique sur « ce qui compte encore comme des mathématiques ». Il s’est assis, a rédigé un billet de blog détaillé, a calculé la quasi-homogénéité du polynôme, proposé une reconstruction géométrique, et même publié l’intégralité de sa discussion avec GPT-5.
C’est l’attitude typique d’un mathématicien de terrain : le résultat est là, on commence par le comprendre, puis on l’utilise.
Tao a souligné dans la discussion HN : « Cela nous apprend que certaines constructions mathématiques apparemment impossibles deviennent trouvables dans un espace de recherche suffisamment vaste. » Le message sous-jacent est crucial : l’espace de recherche est immense, mais l’IA nous enseigne comment y naviguer. Et ce n’est que le début.
Que reste-t-il aux mathématiciens ?
Si l’IA trouve des contre-exemples, vérifie des preuves et formalise des théories entières, que reste-t-il aux mathématiciens humains ?
La réponse de Buzzard : comprendre et interpréter. « La véritable valeur de ces exemples remarquables réside dans la compréhension plus profonde qu’ils apportent aux humains », écrit-il. Akhil Mathew s’efforce déjà de comprendre la structure sous-jacente du contre-exemple de Grothendieck — cherchant à saisir « ce qui se passe vraiment ici », plutôt que de se contenter de constater « une construction aléatoire et un calcul fortuit ».
L’IA peut vous dire que ça ne marche pas, mais elle ne peut généralement pas vous dire ce que ça signifie pour notre vision des mathématiques.
Historiquement, les mathématiciens n’ont cessé de sous-traiter le « calcul » aux machines, pour se concentrer sur des niveaux plus élevés de « compréhension » et de « construction ». Désormais, « trouver des contre-exemples » et « vérifier des preuves » peuvent aussi être sous-traités. Ce qui reste est sans doute le cœur des mathématiques : lorsque la machine dépose un contre-exemple sur la table, comprendre pourquoi il est significatif — et ce que nous pouvons en apprendre.
Ce n’est pas la fin des mathématiques. Mais le rôle du mathématicien est en train de connaître une évolution irréversible.
Références :
- Xenaproject — le billet original de Kevin Buzzard, « Human Mathematicians Are Being Outcounterexampled »
- Discussion HN (id: 48998362) — les réactions de la communauté autour du billet de Terence Tao sur la conjecture jacobienne
- Lobsters (s/wfmpqr) — commentaires approfondis de la communauté technique sur les contre-exemples mathématiques par IA
- Blog de Terence Tao — digestion du contre-exemple de la conjecture jacobienne et reconstruction mathématique
- SBSeminar — discussion des détails mathématiques du nouveau contre-exemple jacobien
- arXiv 2603.19514 — « Learning to Disprove : génération formelle de contre-exemples par grands modèles de langage »
- Article du New Scientist — l’IA résout un problème mathématique vieux de 87 ans
- GitHub DeepMind Formal Conjectures — dépôt de conjectures formalisées, incluant le contre-exemple jacobien
