Three teams posted proofs of a 31-year-old geometry conjecture in October, all using AI

On October 21, 2026, Microsoft Research announced that the Kannan-Lovász-Simonovits conjecture, an open problem in high-dimensional geometry since 1995, had been proved. The authors are Xinzhi Zhang, a senior researcher at Microsoft Research who also signs the post, and Zhao Song, listed on the paper as an independent researcher. According to Microsoft, AI agents explored about a hundred research directions while the two researchers pruned and redirected the search.

Their proof is one of three posted to arXiv between October 4 and October 6. Pierre Bizeul, Boaz Klartag and Joseph Lehec posted theirs about two hours before Song and Zhang’s version 2, and they write that “most proofs and mathematical ideas in this paper were found by ChatGPT.” The third, by Krishnakumar Balasubramanian and Shiva Kasiviswanathan, was developed “with substantial assistance from several frontier AI models.” By October 8, a Lean 4 formalization had appeared on GitHub.

In July, the best known bound still grew with the number of dimensions. Ten weeks later there were three proofs and a machine-checked version, and all three papers disclose the use of AI.

A cut through a high-dimensional blob

The conjecture is about log-concave distributions, a broad family that includes the uniform distribution inside any convex shape and the Gaussian bell curve. Split such a distribution in two along its narrowest bottleneck. KLS predicts that the best flat cut, along a hyperplane, always comes within a fixed factor of the best cut of any shape, whatever the number of dimensions. In the field’s notation, the KLS constant ψ_n stays below a universal constant C.

Microsoft writes that the geometry of these cuts “governs how quickly random walks can explore a distribution,” which ties KLS to high-dimensional sampling and to the speed of randomized algorithms.

Thirty-one years of shrinking bounds

When they stated the conjecture in 1995, Kannan, Lovász and Simonovits proved a bound that grows like the square root of the dimension n. Song and Zhang’s paper lists the progress since then. Yin Tat Lee and Santosh Vempala reached the fourth root of n. In 2021, Yuansi Chen proved the first bound that grows more slowly than any power of n. Klartag and Lehec obtained the first polylogarithmic bound in 2022, and Klartag brought it down to the square root of log n in 2023.

On July 27, 2026, Brayden Letwin posted a bound of log^1/4 n. That was the record when Song and Zhang started.

Ten weeks from Letwin’s bound to a constant

The AI disclosure at the end of Song and Zhang’s 140-page paper gives the timeline. Song first heard of the problem nearly a decade ago and failed twice, as a postdoc at the Institute for Advanced Study around 2019 to 2020 and again from roughly 2022 to 2024. After reading Letwin’s proof, the two authors noticed that the bound might be improved from log^1/4 to log^1/6, and from July 28 they explored “more than 100 approaches in collaboration with AI tools.” The paper names the tools: GPT-6 Astra, GPT-5.6 Sol, Claude Fable 5 and Fable 5.1.

On September 30 they found a route to a bound that depends only on log* n, the number of times a logarithm must be applied to bring n down to 1. For n = 10⁸⁰, log* n is 4. That was version 1, posted October 1. They then applied the same refinement repeatedly, an idea that, according to the paper, was inspired by Song’s earlier work on fast algorithms for linear programs, and proved that the errors added at each round stay bounded in total. Version 2, posted October 4 at 21:21 UTC, proves that ψ_n is at most a universal constant.

Microsoft describes rounds in which several agents explored variations of an idea in parallel and a researcher passed the most promising one to the next round. In a separate track, the authors gave the same problem to several leading models without guidance, with roughly the same total token budget. “That effort fell short of the goal.”

The company credits the recursive method, its repeated application and the bound on accumulated errors to the researchers. AI tools “helped explore candidate approaches, carry out detailed derivations, prepare the manuscript, and perform internal proof checks.” The paper gives joint credit for the first step: candidate approaches were generated collaboratively, the authors chose which ones to prioritize, and “the authors and the AI tools ultimately obtained the log^1/6 bound.” It describes the later steps, the log* route and the repeated refinement, as the authors’ findings.

The ChatGPT acknowledgment

Microsoft calls the authors of the second proof “a separate group of leading experts.” Pierre Bizeul is at the Weizmann Institute of Science, Boaz Klartag at Tel Aviv University and the Weizmann Institute, and Joseph Lehec at Sorbonne Université in Paris. Their 32-page paper, posted October 4 at 19:30 UTC, states in its abstract that “the crucial step in the proof is the very recent criterion from Song and Zhang.”

The acknowledgments go further than Microsoft’s post: “Most proofs and mathematical ideas in this paper were found by ChatGPT; a notable exception is the idea to use suspension which was suggested by the authors. The role of the authors has been mostly to understand these proofs and improve their exposition.” Suspension builds a distribution in a larger dimension from independent copies of the original one. The introduction opens by saying the conjecture “poses little challenge for contemporary AI tools, given the remarkable progress in our understanding of high-dimensional convex bodies in recent decades.”

A third proof and a machine check

On October 6, Balasubramanian and Kasiviswanathan posted a third proof, revised on October 8 to sharpen the bound to an explicit constant: the Poincaré constant is at most 25. Its AI usage statement lists three exchanges in which the authors suggested a direction and the AI built the mathematical tool. Microsoft says this proof “relies on a closely related idea.”

On October 8, a repository named KLS500 appeared on GitHub with a Lean 4 formalization of a dimension-free Poincaré bound of 500 for every isotropic log-concave distribution. Lean is a proof assistant: it accepts a proof only when every step passes its logical kernel. The README says the work mainly follows the Bizeul-Klartag-Lehec approach, Song-Zhang criterion included, that the verification “rebuilt 1,710 mathematical modules at kernel trust level zero,” and that it also checks the exact KLS statement OpenAI published in its public math repository.

The open checks

None of the three papers, all arXiv preprints, has been peer reviewed. Song and Zhang’s shortened proof and its Lean check, announced in Microsoft’s post, have not been released: the authors “plan to release both after final review.” KLS500 sits on a personal GitHub account and names no institution, and its README says that Comparator and Nanoda were not run. Both are tools that recheck a Lean proof outside the standard build.

The comparison with unguided models comes from the authors alone, and Microsoft’s post does not say which models ran, how many attempts were made or what the budget was. The ChatGPT credit covers one 32-page paper whose crucial step, by its own account, came from Song and Zhang, and the paper does not say which ChatGPT model was used. Song and Zhang write that all of their proofs “have been carefully verified by the authors and several AI tools” and that they “take full responsibility for the correctness of the proofs.”

What it means

The three teams split the credit differently. In Microsoft’s account, people chose the directions and supplied the decisive ideas, and models working alone on a similar budget did not get there. In the Bizeul-Klartag-Lehec paper, the authors describe their main job as understanding ChatGPT’s proofs and writing them up. Balasubramanian and Kasiviswanathan single out three exchanges in which they suggested a direction and the AI built the tool.

In recent weeks, AI-assisted work in physics produced explicit counterexamples to a 1967 fusion conjecture, and a physicist used Claude to recheck a year of his PhD calculations in about 10 hours. At Harvard, Matthew Schwartz described a similar division of labor for 36 manuscripts, with a specialist checking everything.

Song and Zhang’s criterion, posted October 1, became the base of a second group’s proof three days later and of a Lean formalization four days after that, while none of the three papers has yet been through peer review.

The next markers are peer review of the three papers, the release of Song and Zhang’s shortened proof with its Lean check, and runs of Comparator and Nanoda on KLS500. None of the three papers includes the prompts or transcripts behind its results, so how much each model contributed, step by step, is still known only from the authors’ own descriptions.

Sources

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

Header image: chart by MACCUS, data from Song and Zhang, arXiv:2610.01447, Table 1 (October 4, 2026)