En mai 2026, OpenAI a annoncé qu'un de ses modèles internes avait réfuté une conjecture de Paul Erdős vieille de près de quatre-vingts ans. De l'extérieur, la nouvelle a de quoi impressionner : une intelligence artificielle qui « résout » un problème ouvert célèbre, là où des générations de mathématiciens avaient buté. Mais que signifie exactement « résoudre » ? Sept mois plus tôt, une annonce du même genre s'était effondrée sous les moqueries de la communauté. Pour démêler l'authentique de la publicité, Next a interrogé la mathématicienne Viviane Pons et son confrère David Madore. Leurs réponses dessinent un tableau bien plus nuancé que les communiqués triomphants.

L'annonce qui a secoué la communauté

Le 21 mai 2026, OpenAI publie un billet au titre sobre : un de ses modèles a réfuté une conjecture de géométrie discrète. Il ne s'agit pas d'un système spécialisé dans les mathématiques, ni d'un démonstrateur formel, mais d'un modèle de raisonnement généraliste — un « grand modèle de langage » (LLM), qui raisonne en langage naturel. On lui a soumis un problème, sans indice ni piste, et il a produit une démonstration de trois pages.

Le résultat n'est pas anodin. Contrairement à la déconvenue d'octobre 2025 (nous y reviendrons), la preuve a été prise très au sérieux. Neuf mathématiciens de premier plan — parmi lesquels Noga Alon, Melanie Wood, Will Sawin ou Thomas Bloom — l'ont examinée en détail et cosigné un document, « Remarks on the disproof of the unit distance conjecture », qui en propose une version nettoyée et simplifiée. Le médaillé Fields Timothy Gowers a jugé qu'« aucune preuve produite par une IA n'en avait jusqu'ici approché » le niveau, rapporte le Scientific American. Daniel Litt, de l'université de Toronto, y voit « le seul résultat vraiment intéressant produit de façon autonome par une IA à ce jour ». C'est, de fait, une première : jusque-là, aucune IA n'avait apporté aux mathématiques un résultat nouveau et significatif.

Un problème vieux de quatre-vingts ans

De quoi parle-t-on au juste ? Le « problème des distances unités » (unit distance problem) a été formulé par Paul Erdős en 1946, et le collectionneur de conjectures le comptait parmi ses préférés. L'énoncé est d'une simplicité trompeuse : on place n points dans le plan, et on cherche à maximiser le nombre de paires de points situées exactement à distance 1. Combien peut-on en obtenir quand n devient grand ?

Une grille carrée de côté 1 donne déjà, grossièrement, deux fois plus de paires à distance 1 qu'il n'y a de points. La question est de savoir si l'on peut faire significativement mieux. Erdős était fermement convaincu que non : il conjecturait qu'on ne pouvait pas dépasser un nombre de paires de l'ordre de n¹⁺ᵒ⁽¹⁾, c'est-à-dire à peine plus que n. La meilleure borne supérieure connue, due à Spencer, Szemerédi et Trotter en 1984, était de l'ordre de n⁴ᐟ³.

Ce que le modèle d'OpenAI a démontré, comme l'explique David Madore sur son blog, c'est qu'il existe un exposant ε strictement positif tel qu'on peut construire, pour des n arbitrairement grands, des ensembles de points ayant au moins n¹⁺ᵋ paires à distance 1. Autrement dit : Erdős avait tort, et les configurations optimales peuvent être bien plus denses que l'intuition ne le laissait croire. La construction passe par un réseau en dimension supérieure, doté de symétries algébriques, « aplati » ensuite dans le plan — un objet trop complexe pour être dessiné à la main. L'ε obtenu est d'ailleurs minuscule, de l'ordre de 6×10⁻³⁸ : le résultat est spectaculaire sur le plan conceptuel, invisible à l'œil nu.

Madore, mathématicien et maître de conférences, situe la portée du résultat avec précision : il le juge « assez comparable en importance » au progrès réalisé en 2018 par Aubrey de Grey sur le problème voisin de Hadwiger-Nelson. « C'est surprenant, ça montre qu'on avait une mauvaise intuition sur les unit distance graphs, mais en fait ça n'améliore pas vraiment notre compréhension de ces graphes », écrit-il. Un beau résultat, digne d'un excellent journal — pas une révolution.

« Résoudre » : un mot à manier avec des pincettes

Toute la difficulté tient dans ce verbe. Car sept mois plus tôt, en octobre 2025, OpenAI avait déjà claironné une percée qui s'était retournée contre elle. Le vice-président Kevin Weil affirmait dans un message — depuis effacé — que GPT-5 avait « trouvé des solutions à 10 (!) problèmes d'Erdős jusque-là non résolus » et progressé sur onze autres.

La riposte fut cinglante. Thomas Bloom, le mathématicien qui maintient le site de référence erdosproblems.com, a qualifié l'affirmation de « déformation spectaculaire » : sur son site, « ouvert » signifie seulement qu'il ignorait personnellement une solution. GPT-5 n'avait rien démontré de neuf ; il avait retrouvé, dans la littérature, des articles déjà publiés qui résolvaient ces problèmes — dont les auteurs eux-mêmes ignoraient qu'ils réglaient une question cataloguée comme importante. Un travail de moteur de recherche, pas de création. Yann LeCun, chez Meta, a raillé des chercheurs « victimes de leurs propres GPTards » ; Demis Hassabis, patron de Google DeepMind, a lâché : « C'est embarrassant. »

Cet épisode éclaire l'expérience quotidienne de Madore. « Pour la réflexion mathématique, je les ai trouvés totalement inutiles à part comme une sorte de moteur de recherche amélioré », écrit-il à propos des LLM qu'il utilise (surtout en version gratuite). Dès qu'il soumet un vrai problème non trivial, il obtient « une réponse très assurée, superficiellement plausible, et en fait complètement bidon ». Le contraste entre ce vécu et les annonces spectaculaires est au cœur du malaise : le niveau réel des modèles en mathématiques dépend de tant de paramètres — qui évalue, quoi, comment, avec quel modèle, quel budget — qu'« il faut prendre ces annonces un peu comme quand une compagnie pharmaceutique prétend avoir guéri quelqu'un d'une maladie incurable ». C'est peut-être significatif, mais tant qu'on ne dispose d'aucun détail technique, « c'est juste une pub ».

Pourquoi la machine a réussi là où les humains ont échoué

Si le résultat de mai 2026 est authentique, il reste à comprendre pourquoi aucun humain n'avait trouvé ce contre-exemple. Et là, la démystification est instructive. La preuve, souligne Madore après l'avoir lue dans sa version simplifiée par les mathématiciens, « ne contient aucune idée majeure, aucune construction nouvelle, et rien qui ne paraîtrait surhumain de quelque manière que ce soit ». Les outils employés — corps CM, théorie du corps de classes, théorème de densité de Čebotarëv, inégalité de Golod-Šafarevič — relèvent d'un cours de deuxième année de master en théorie algébrique des nombres. L'apport du modèle tient à deux petits lemmes, « faciles à démontrer », mais qu'il fallait « penser » à introduire.

Trois raisons, selon lui, expliquent la victoire de la machine. D'abord, elle « n'était pas influencée par l'intuition d'Erdős » : persuadés que la conjecture était vraie, les humains ont cherché à la prouver plutôt qu'à la réfuter. Ensuite, le modèle dispose d'une « connaissance encyclopédique des mathématiques », là où produire ce contre-exemple exigeait de marier une connaissance fine du problème et des techniques pointues de théorie des nombres — un croisement que peu de spécialistes maîtrisent. Enfin, il a « une patience inépuisable pour tester les pistes de façon exhaustive », sans se décourager devant un calcul fastidieux et a priori voué à l'échec. En revanche, « pas de trace d'intuition fulgurante, de technique nouvelle, encore moins de génie surhumain ». La preuve la plus parlante de cette modestie : le mathématicien Will Sawin a amélioré l'exposant dès le lendemain de l'annonce. « Il ne faut ni surestimer ce résultat — les LLM actuels ne sont absolument pas surhumains en maths — ni le sous-estimer : ce ne sont pas non plus des perroquets stochastiques », résume Madore.

Le pari de Terence Tao : faire de l'IA un ouvrier, pas un oracle

Face à ces débats, une figure occupe une position à part : Terence Tao, sans doute le mathématicien vivant le plus célèbre, devenu un « évangéliste » de l'IA en mathématiques — non par naïveté, mais par méthode. Tao ne demande pas aux modèles de trouver seuls de grands théorèmes. Il les décrit sans ménagement comme des « étudiants trop sûrs d'eux, qui font des suggestions sans avoir l'expertise de distinguer les bonnes des mauvaises idées », et rappelle qu'ils « calent » dès qu'on approche des frontières de la recherche, là où les données d'entraînement se raréfient.

Sa réponse tient en trois mots : formalisation, division, vérification. Tao a appris dès 2023 le langage Lean, un assistant de preuve dans lequel une démonstration devient un objet informatique que la machine valide — ou refuse. Son projet phare, l'Equational Theories Project, a mobilisé une cinquantaine de contributeurs pour trancher et vérifier en Lean quelque 22 millions d'implications entre lois algébriques, faisant même émerger un objet inédit, la « cohomologie des magmas ». Le modèle qu'il défend est hybride : à l'IA les « milliers de sous-problèmes petits et gérables », à Lean la garantie de correction, aux humains les questions les plus difficiles et le choix des directions.

Cette philosophie recoupe une conviction de Madore. « C'est sur cet aspect des maths que j'avais le plus d'espoir en l'IA : non pas pour trouver de nouvelles preuves, mais pour vérifier formellement les preuves existantes. » La formalisation par LLM est, selon lui, « exactement le genre de choses auxquelles ils sont censés servir » : peu importe que le modèle hallucine en traduisant une preuve en Lean, puisque l'assistant refusera tout ce qui est faux. Reste que le progrès s'est fait à l'envers : « On a automatisé une partie intéressante des maths plus vite qu'une partie fastidieuse. C'est très con, ça. »

Preuves « bidon » et noyade sous l'AI slop

Car la première menace que les chercheurs identifient n'est pas celle d'IA surpuissantes, mais celle d'IA médiocres et prolixes. Madore observe déjà l'effet le plus visible des LLM sur son quotidien : MathOverflow, forum de référence, « reçoit plein de réponses générées par LLM qui semblent superficiellement plausibles » mais recèlent « des erreurs fondamentales ». Le danger est sournois, car ces erreurs « ne ressemblent pas à celles que font les humains » du niveau d'expertise que le ton du texte laisse supposer : un modèle invoquera un théorème « en omettant de vérifier ses hypothèses », ce qu'un vrai spécialiste ne ferait pas.

L'enjeu dépasse le forum. Toute la vérification mathématique repose sur une confiance implicite : quand un article affirme qu'« un calcul évident montre que… », le relecteur — bénévole et anonyme — ne recontrôle pas tout, parce qu'il suppose l'auteur faillible mais de bonne foi. Les LLM font sauter ce contrat. Si la prolifération de preuves plausibles-mais-fausses oblige un jour à tout formaliser, y compris ce que produisent les humains « parce qu'on ne peut plus jamais en être sûr », « ce sera un recul énorme de nos capacités », prévient Madore. Le fossé entre ce qu'on sait formaliser en Lean et ce qu'on démontre en langage naturel reste, pour l'heure, « énorme ». Plus largement, la littérature scientifique se fait « noyer par l'AI slop », références hallucinées comprises.

Ce qui inquiète vraiment les chercheurs

Reste la menace la plus profonde, et la plus politique. Interrogée par Next, Viviane Pons — chercheuse à l'université Paris-Saclay, spécialiste de combinatoire et praticienne de longue date de l'« exploration par ordinateur » comme outil d'expérimentation mathématique — déplace le regard vers les conditions matérielles de la recherche. Militante de la science ouverte et du logiciel libre, elle alerte sur les enjeux éthiques et environnementaux d'une dépendance croissante à des outils très gourmands en énergie et en ressources, contrôlés par une poignée d'entreprises privées. La question du coût — écologique autant qu'économique — n'est pas un à-côté : elle conditionne l'accès même à ces technologies.

Madore prolonge cette inquiétude jusqu'au bout. Le risque, écrit-il, n'est pas tant que l'IA rende les mathématiciens « obsolètes » — « si on me donne un gadget magique qui produit une preuve élégante de n'importe quel théorème, moi je vais m'en réjouir » — que de « détruire les fondements économiques de la pratique de la recherche », ou de la « réserver aux plus riches, qui pourront se payer l'accès aux IA deluxe ». D'où sa défiance devant les silences d'OpenAI : combien de problèmes le modèle a-t-il échoué à résoudre avant celui-ci ? Combien de temps de calcul, quel coût, quelle consommation d'énergie pour cette seule démonstration ? Pourquoi cette focalisation sur les problèmes d'Erdős, qui « surreprésentent la combinatoire et la théorie des nombres élémentaire » au détriment de pans entiers des mathématiques ? Autant de questions dont « le silence est extrêmement suspect ».

Le tableau qui se dégage de ces voix croisées n'est donc ni celui de l'apocalypse ni celui du paradis annoncé. Une IA a bel et bien produit, pour la première fois, un résultat mathématique nouveau et vérifié — fait notable, à ne pas balayer. Mais elle l'a fait sans génie, par force brute encyclopédique et patience, sur un problème choisi et présenté par une entreprise dont le métier est de vendre. Entre la promesse d'un assistant qui libérerait les chercheurs des tâches ingrates et le cauchemar d'une discipline noyée sous les preuves douteuses ou privatisée au profit des mieux dotés, les mathématiciens interrogés refusent de trancher trop vite. Ils demandent surtout ce que réclame toute science : de la transparence, des protocoles, et le droit d'exercer leur esprit critique face aux annonces — d'où qu'elles viennent.