Trois preuves d’une conjecture de géométrie vieille de 31 ans déposées en octobre, toutes avec l’IA

Le 21 octobre 2026, Microsoft Research a annoncé la démonstration de la conjecture de Kannan, Lovász et Simonovits (KLS), un problème de géométrie en grande dimension ouvert depuis 1995. Ses auteurs sont Xinzhi Zhang, chercheuse senior chez Microsoft Research et signataire du billet, et Zhao Song, présenté dans la prépublication comme chercheur indépendant. Selon Microsoft, des agents d’IA ont exploré une centaine de pistes, que les deux chercheurs triaient et réorientaient.

Deux autres preuves ont été déposées sur arXiv les 4 et 6 octobre. La deuxième, signée par Pierre Bizeul, Boaz Klartag et Joseph Lehec (Sorbonne Université) et mise en ligne environ deux heures avant la version 2 de Song et Zhang, précise que « la plupart des démonstrations et des idées mathématiques de cet article ont été trouvées par ChatGPT ». La troisième, de Krishnakumar Balasubramanian et Shiva Kasiviswanathan, a été mise au point « avec une aide substantielle de plusieurs modèles d’IA de pointe ».

En juillet, la meilleure borne connue augmentait encore avec le nombre de dimensions. Dix semaines plus tard, on comptait trois preuves et une vérification par machine, et les trois articles font état d’un recours à l’IA.

Une coupe en grande dimension

La conjecture porte sur les lois log-concaves, une large famille qui comprend la loi uniforme sur tout corps convexe et la loi gaussienne. On coupe une telle loi en deux à son goulet le plus étroit. KLS prédit que la meilleure coupe plane, le long d’un hyperplan, reste toujours à un facteur fixe près de la meilleure coupe de forme quelconque, quel que soit le nombre de dimensions.

Microsoft écrit que la forme de ces coupes « détermine la vitesse à laquelle des marches aléatoires peuvent explorer une distribution », ce qui relie KLS à l’échantillonnage en grande dimension et à la rapidité des algorithmes probabilistes.

Trente et un ans de bornes

En formulant leur conjecture en 1995, Kannan, Lovász et Simonovits ont démontré une borne qui croît comme la racine carrée de la dimension n. Depuis, selon l’article de Song et Zhang, Yin Tat Lee et Santosh Vempala sont descendus à la racine quatrième de n. En 2021, Yuansi Chen a obtenu la première borne qui croît moins vite que toute puissance de n. Klartag et Lehec ont établi la première borne polylogarithmique en 2022, puis Klartag l’a ramenée à la racine carrée de log n en 2023.

Le 27 juillet 2026, Brayden Letwin a publié une borne en log^1/4 n. C’était le record quand Song et Zhang se sont lancés.

Dix semaines entre la borne de Letwin et une constante

La note sur l’usage de l’IA, à la fin de l’article de 140 pages de Song et Zhang, donne la chronologie. Song connaissait le problème depuis près de dix ans et avait échoué deux fois, vers 2019-2020 en postdoctorat à l’Institute for Advanced Study, puis entre 2022 et 2024 environ. Après avoir lu la preuve de Letwin, les deux auteurs ont entrevu qu’il serait peut-être possible de passer de log^1/4 à log^1/6. À partir du 28 juillet, ils ont exploré « plus de 100 approches en collaboration avec des outils d’IA ». L’article les nomme : GPT-6 Astra, GPT-5.6 Sol, Claude Fable 5 et Fable 5.1.

Le 30 septembre, ils ont trouvé un moyen d’obtenir une borne qui ne dépend plus que de log* n, le nombre de logarithmes successifs nécessaires pour ramener n à 1. Pour n = 10⁸⁰, log* n vaut 4. C’est la version 1, mise en ligne le 1er octobre. Ils ont ensuite répété le même raffinement, une idée inspirée, selon l’article, des travaux antérieurs de Song sur les algorithmes rapides de programmation linéaire, et prouvé que les erreurs ajoutées à chaque tour restent bornées au total. La version 2, déposée le 4 octobre à 21 h 21 UTC, démontre que la constante KLS est majorée par une constante universelle.

Selon le billet, les auteurs ont aussi confié le même problème à plusieurs grands modèles, sans guidage et avec un budget de tokens comparable. Cette tentative « n’a pas atteint l’objectif ».

Microsoft attribue aux chercheurs la méthode récursive, son application répétée et la preuve que les erreurs accumulées restent bornées ; l’IA, elle, a aidé à explorer des pistes, à mener les calculs détaillés, à préparer le manuscrit et à vérifier les preuves en interne. Pour la première étape, l’article décrit un travail commun : les approches candidates ont été produites ensemble, les auteurs choisissaient lesquelles privilégier, et « les auteurs et les outils d’IA ont finalement obtenu la borne en log^1/6 ». Il présente les étapes suivantes, la piste en log* et le raffinement répété, comme des trouvailles des auteurs.

Les remerciements à ChatGPT

Pierre Bizeul travaille à l’Institut Weizmann des sciences, Boaz Klartag à l’université de Tel-Aviv et à l’Institut Weizmann, et Joseph Lehec à Sorbonne Université, à Paris. Leur article de 32 pages, déposé le 4 octobre à 19 h 30 UTC, indique dès le résumé que « l’étape cruciale de la preuve est le critère très récent de Song et Zhang ».

Les remerciements vont plus loin que le billet de Microsoft : « La plupart des démonstrations et des idées mathématiques de cet article ont été trouvées par ChatGPT ; une exception notable est l’idée d’utiliser la suspension, suggérée par les auteurs. Le rôle des auteurs a surtout consisté à comprendre ces démonstrations et à en améliorer l’exposition » (notre traduction). La suspension construit une loi en dimension plus grande à partir de copies indépendantes de la loi de départ. La première phrase de l’introduction affirme que la conjecture « pose peu de difficultés aux outils d’IA actuels, compte tenu des progrès remarquables de notre compréhension des corps convexes en grande dimension ces dernières décennies ».

Une troisième preuve et une vérification par machine

Le 6 octobre, Balasubramanian et Kasiviswanathan ont déposé une troisième preuve, révisée le 8 octobre pour resserrer la borne à une constante explicite : la constante de Poincaré vaut au plus 25. Leur déclaration sur l’usage de l’IA décrit trois échanges : les auteurs proposaient une direction, l’IA construisait l’outil mathématique. Selon Microsoft, cette preuve « repose sur une idée très proche ».

Le 8 octobre est apparu sur GitHub le dépôt KLS500, qui formalise en Lean 4 une borne de Poincaré égale à 500, indépendante de la dimension, pour toute loi log-concave isotrope. Lean est un assistant de preuve : il n’accepte une démonstration que si chaque étape est validée par son noyau logique. Le fichier de présentation indique que le travail suit surtout l’approche de Bizeul, Klartag et Lehec, critère de Song et Zhang compris, que la vérification « a recompilé 1 710 modules mathématiques » au niveau de confiance zéro du noyau, et qu’elle valide aussi l’énoncé exact de KLS qu’OpenAI a publié dans son dépôt public de mathématiques.

Les vérifications qui manquent

Aucune des trois prépublications arXiv n’a été relue par des pairs. La preuve raccourcie de Song et Zhang et sa vérification en Lean, annoncées dans le billet de Microsoft, n’ont pas été publiées : les auteurs prévoient de diffuser les deux « après une dernière relecture ». KLS500 est hébergé sur un compte GitHub personnel qui ne cite aucune institution, et son fichier de présentation précise que Comparator et Nanoda n’ont pas été lancés. Ces deux outils revérifient une preuve Lean en dehors de la compilation standard.

La comparaison avec les modèles livrés à eux-mêmes ne repose que sur le récit des auteurs, et le billet ne dit ni quels modèles ont servi, ni combien d’essais ont été faits, ni quel était le budget. Le mérite attribué à ChatGPT ne concerne qu’un article, dont l’étape cruciale vient, selon ses auteurs, de Song et Zhang, et qui ne précise pas quel modèle de ChatGPT a servi. Song et Zhang écrivent que toutes leurs démonstrations « ont été soigneusement vérifiées par les auteurs et par plusieurs outils d’IA » et qu’ils assument « l’entière responsabilité de leur exactitude ».

Notre analyse

Les trois équipes répartissent le mérite différemment. Dans le récit de Microsoft, les humains ont choisi les directions et apporté les idées décisives, et des modèles laissés seuls avec un budget comparable n’y sont pas parvenus. Dans l’article de Bizeul, Klartag et Lehec, les auteurs disent avoir surtout compris et rédigé les démonstrations de ChatGPT. Balasubramanian et Kasiviswanathan retiennent trois échanges dans lesquels ils proposaient une direction et l’IA construisait l’outil.

Ces dernières semaines, en physique, des travaux menés avec l’IA ont produit des contre-exemples explicites à une conjecture de 1967 sur la fusion, et un physicien a revérifié avec Claude un an de calculs de thèse en une dizaine d’heures. À Harvard, Matthew Schwartz a décrit un partage des tâches comparable pour 36 manuscrits, avec un spécialiste qui vérifie tout.

Le critère de Song et Zhang, publié le 1er octobre, a servi de base à la preuve d’un autre groupe trois jours plus tard, puis à une formalisation en Lean quatre jours après, alors qu’aucun des trois articles n’est encore passé par la relecture par les pairs.

Les prochains repères sont la relecture des trois articles par des pairs, la publication de la preuve raccourcie de Song et Zhang avec sa vérification en Lean, et le passage de KLS500 dans Comparator et Nanoda. Aucun des trois articles ne publie les requêtes ni les échanges avec les modèles, si bien que la part exacte de chaque modèle, étape par étape, n’est connue que par le récit des auteurs.

Sources

• Solving a 31-year-old grand challenge in mathematics: the KLS conjecture, Xinzhi Zhang, blog de Microsoft Research, 21 octobre 2026
• An O(1) Bound for the KLS Constant, Z. Song et X. Zhang, arXiv, 4 octobre 2026 (version 2)
• Presenting a proof of the Kannan-Lovasz-Simonovits conjecture, P. Bizeul, B. Klartag et J. Lehec, arXiv, 4 octobre 2026
• A Dimension-Free Bound on the Poincaré Constant of Isotropic Log-Concave Measures, K. Balasubramanian et S. Kasiviswanathan, arXiv, 8 octobre 2026 (version 2)
• The KLS constant is O(log^1/4 n), B. Letwin, arXiv, 27 juillet 2026
• HongruZhao/KLS500, GitHub, 8 octobre 2026
• OAI/Analysis/KLS/Model.lean, OpenAI, dépôt openai/math sur GitHub, 6 octobre 2026

Image d’en-tête : graphique MACCUS, données Song et Zhang, arXiv:2610.01447, tableau 1 (4 octobre 2026)