La conjecture KLS, énigme mathématique de 31 ans, résolue avec l’aide de l’IA

Pendant trente et un ans, la question a résisté aux meilleurs spécialistes de la géométrie. Le 21 octobre 2026, Microsoft Research a annoncé sur son blog que la conjecture de Kannan, Lovász et Simonovits, dite conjecture KLS, était démontrée. L’annonce intervient trois semaines après la mise en ligne d’une prépublication de 140 pages, et elle n’est pas isolée : une autre équipe de mathématiciens a publié sa propre preuve, en expliquant sans détour que l’essentiel des idées venait de ChatGPT. Pour la première fois, un problème de cette envergure semble céder grâce à une collaboration étroite entre chercheurs et intelligence artificielle.

Que dit la conjecture KLS ?

La conjecture a été formulée en 1995 par trois chercheurs en informatique théorique et en mathématiques, Ravi Kannan, László Lovász et Miklós Simonovits. Elle concerne des objets dits « convexes », c’est-à-dire sans creux ni trou, comme une balle ou un cube, mais considérés dans des espaces qui comptent des centaines ou des milliers de dimensions. Plus précisément, elle porte sur une large famille de distributions de probabilité dites log-concaves, qui généralisent ces formes.

La question peut se résumer ainsi : quelle est la meilleure façon de couper un tel objet en deux morceaux, avec une coupe la plus petite possible au regard de la taille des morceaux obtenus ? Le blog de Microsoft Research résume la conjecture en une phrase : la meilleure coupe plane est toujours presque aussi efficace que la meilleure coupe de forme quelconque, avec un écart borné par une constante universelle, quelle que soit la dimension. Autrement dit, même dans un espace à un million de dimensions, inutile de chercher des découpes tordues : une simple tranche fait presque aussi bien.

Pourquoi ce problème compte au-delà des mathématiciens

L’enjeu n’est pas seulement théorique. La conjecture est née dans l’étude d’algorithmes qui mesurent le volume de formes convexes en se promenant au hasard à l’intérieur. La géométrie des coupes détermine la vitesse à laquelle une telle marche aléatoire explore tout l’espace : si une forme possède un goulot d’étranglement, le marcheur risque d’y rester coincé d’un côté.

C’est pourquoi Microsoft Research souligne le rôle central de la conjecture dans la théorie de l'échantillonnage en grande dimension, une famille de méthodes qui consistent à tirer des points au hasard pour estimer des quantités impossibles à calculer directement. Ces techniques servent en statistique, en optimisation et en apprentissage automatique. Selon le laboratoire, de nombreux résultats qui supposaient la conjecture vraie pourront désormais être énoncés sans condition.

Le chemin a été long. En 2013, le mathématicien Ronen Eldan introduisait une technique dite de localisation stochastique, qui a relancé les recherches. En 2020, Yuansi Chen obtenait une borne « presque constante », une avancée saluée comme majeure. Il restait pourtant à franchir la dernière marche : montrer que l’écart ne grandit pas du tout avec la dimension.

Comment l’IA a contribué aux preuves

La prépublication principale, intitulée « An O(1) Bound for the KLS Constant », est signée par Xinzhi Zhang, chercheur dans le groupe apprentissage automatique et optimisation de Microsoft Research, et Zhao Song. Elle a été déposée sur arXiv, la plateforme de prépublications scientifiques, le 1er octobre 2026, puis révisée le 4 octobre.

Selon le blog de Microsoft Research, les auteurs ont suivi un processus de recherche « agentique dirigé par des humains » : plusieurs agents d’IA exploraient des variantes en parallèle, les chercheurs examinaient les résultats intermédiaires et abandonnaient les pistes peu prometteuses. Environ une centaine de trajectoires de recherche ont été explorées avant la percée décisive, dont beaucoup impliquaient de lourds calculs sur des tenseurs, des tableaux de nombres à plusieurs dimensions.

Le partage des rôles est décrit précisément. Les outils d’IA ont exploré les approches candidates, mené les calculs détaillés, aidé à préparer le manuscrit et effectué des vérifications internes de la preuve. Les chercheurs, eux, « ont déterminé la direction mathématique, sélectionné les idées prometteuses, assemblé l’argument final et vérifié la preuve », écrit Xinzhi Zhang. Microsoft ne précise pas quels modèles ont été utilisés. Le laboratoire signale en revanche qu’une tentative menée avec plusieurs modèles de pointe laissés sans direction humaine, avec un budget de calcul comparable, n’a pas atteint le but.

Une seconde preuve écrite en grande partie par ChatGPT

Le 4 octobre 2026, trois mathématiciens, Pierre Bizeul, Boaz Klartag et Joseph Lehec, ont déposé sur arXiv une preuve indépendante de 32 pages. Leur résumé indique que l’étape cruciale repose sur le critère tout récent de Song et Zhang, ce qui en fait un prolongement de la première prépublication plutôt qu’un travail totalement séparé.

Leurs remerciements contiennent une phrase rare dans une publication de ce niveau : « la plupart des preuves et des idées mathématiques de cet article ont été trouvées par ChatGPT », la principale exception étant une construction géométrique, la suspension, suggérée par les auteurs. Les trois chercheurs décrivent leur propre rôle comme ayant surtout consisté à comprendre ces preuves et à en améliorer la présentation.

Une troisième démonstration, signée Krishnakumar Balasubramanian et Shiva Kasiviswanathan, a été déposée le 6 octobre et s’appuie sur une idée proche. Pour Microsoft Research, l’existence de plusieurs preuves renforce la confiance, puisque le résultat ne repose plus sur un seul raisonnement.

La preuve est-elle vraiment validée ?

Pas encore au sens habituel. Ces trois textes sont des prépublications : ils n’ont pas été relus et acceptés par une revue scientifique, une étape qui prend souvent des mois pour des preuves aussi longues. La communauté mathématique a toutefois plusieurs raisons de les prendre au sérieux : l’implication de spécialistes reconnus du domaine, comme Boaz Klartag, la convergence de plusieurs démonstrations et l’apparition de vérifications informatiques.

Selon Microsoft Research, une formalisation dans Lean, un logiciel qui vérifie mécaniquement chaque étape d’une démonstration, a été publiée par d’autres chercheurs. Elle s’appuie principalement sur l’approche de Bizeul, Klartag et Lehec, en y intégrant le critère de Song et Zhang. Les auteurs de Microsoft disent avoir eux-mêmes raccourci leur preuve et vérifié cette version simplifiée dans Lean, et prévoient de la publier après une dernière relecture.

Ce que cela change pour la recherche mathématique

Cette percée prolonge une série d’avancées spectaculaires, des performances de niveau médaille d’or de Gemini aux Olympiades internationales de mathématiques en 2025 aux premiers résultats de recherche obtenus avec des modèles de langage. La différence est de taille : il ne s’agit plus d’exercices de compétition dont la solution est connue, mais d’un problème ouvert depuis trois décennies, étudié par des chercheurs de premier plan.

Les deux récits dessinent aussi deux manières de travailler. Chez Microsoft, l’IA sert de force d’exploration massive, encadrée à chaque étape par des chercheurs qui trient les idées. Chez Bizeul, Klartag et Lehec, le modèle propose l’essentiel des arguments et les mathématiciens jouent le rôle de lecteurs critiques et de rédacteurs. Dans les deux cas, l’expertise humaine reste indispensable pour savoir quelle question poser, reconnaître une piste prometteuse et vérifier le résultat.

Des questions restent ouvertes, à commencer par la manière de créditer les contributions de l’IA dans les publications et par l’avenir de la vérification, alors que des preuves de plus en plus longues pourraient être produites plus vite que les spécialistes ne peuvent les relire. Les outils de vérification formelle comme Lean deviennent, dans ce contexte, un complément de plus en plus central. Les articles de la page mathématiques d’Actu.ai retracent les étapes qui ont mené à ce point.