Microsoft researchers used AI agents to help prove the 31-year-old KLS conjecture

What Microsoft announced

Microsoft Research said on 21 October 2026 that one of its researchers and a collaborator have proved the Kannan-Lovász-Simonovits conjecture, a problem in high-dimensional geometry first posed in 1995. In a blog post, senior researcher Xinzhi Zhang described the result as settling "a 31-year-old problem widely regarded as one of the central open questions in high-dimensional geometry." The proof is by Zhang and Zhao Song, and it sits in a 140-page preprint on arXiv called An O(1) Bound for the KLS Constant.

The headline for most readers is how the work was done. Microsoft calls it "a human-directed agentic research process in which AI systems explored mathematical possibilities while researchers evaluated, pruned, and redirected the search." The company also reports a control experiment that went the other way: when the authors gave several leading AI models roughly the same token budget and let them work on the problem unguided, the models fell short.

The math itself is not new as of this week. The decisive version of the paper went up on 4 October, and two other groups posted proofs within days. What the 21 October post adds is Microsoft's own account of the process, the claim of independent confirmation, and a promise to release a shorter proof that the authors say they have checked in the Lean proof assistant.

What the KLS conjecture says

The KLS conjecture is about how hard it is to split a high-dimensional shape, or more generally a spread of probability, into two large pieces with a small boundary between them. The narrowest such boundary is a bottleneck. You can look for it with any curved cut you like, or only with flat cuts, which mathematicians call hyperplanes.

Kannan, Lovász and Simonovits guessed that for a broad class of distributions, called log-concave, the best flat cut is always within a fixed factor of the best cut of any shape, no matter how many dimensions there are. Log-concave distributions include the uniform distribution on any convex body, such as a cube, a ball or the tetrahedron shown above, and the bell-curve Gaussian. In the paper's language, the KLS constant is bounded by a universal number.

This matters outside pure geometry because the same bottlenecks control how fast random-walk algorithms mix. Those algorithms are used to sample from distributions, estimate volumes and run optimisation in many dimensions. Microsoft says a wide range of results that assumed KLS "can now be stated unconditionally." Earlier bounds were close but still grew slowly with dimension. The best one before this work, posted by Brayden Letwin on 27 July 2026, grew like the fourth root of the logarithm of the dimension.

How the proof came together

The paper's acknowledgements give an unusually detailed history. Song writes that he first heard of the problem nearly a decade ago and tried it without success around 2019 to 2020 and again from roughly 2022 to 2024. After reading Letwin's July preprint, the authors saw a chance to improve its bound, and from 28 July 2026 they "explored more than 100 approaches in collaboration with AI tools." That work first produced a slightly better bound, then a new criterion that Microsoft calls "the foundation of the final proof."

On 30 September the authors found that the criterion could be fed back into itself. Each improved bound produced a tighter one, which brought the dependence on dimension down to the iterated logarithm, a function that grows almost unimaginably slowly but still grows. That is version one of the paper, posted on 1 October. The last step was to repeat the whole refinement and show that the small losses at each stage shrink fast enough to add up to a fixed constant. That closed the gap in version two, posted on 4 October. The authors credit ideas from Song's earlier work on fast linear-programming algorithms and from a technique in fine-grained complexity.

How the AI was used

Microsoft is careful about where it draws the line. The recursive method, its repeated application and the proof that the errors stay bounded "are original contributions of the researchers," the blog says. AI tools "helped explore candidate approaches, carry out detailed derivations, prepare the manuscript, and perform internal proof checks," while the researchers chose the direction, selected ideas, assembled the argument and verified it.

The paper names the tools: "GPT-6 Astra, GPT-5.6 Sol, Claude Fable 5, and Fable 5.1." The workflow Microsoft describes is a loop. Several agents explored variations of an idea in parallel, a researcher read their intermediate results, cut the weak directions and passed the most promising result to the next round. About 100 such research trajectories ran before the key step appeared.

The control run is the most useful detail for anyone judging AI claims in mathematics. Microsoft says unguided attempts with several leading models, at roughly the same total token budget, "fell short of the goal." That is one team's report, not a benchmark, but it fits a pattern seen in other recent results, such as the Intern-S2 work on the Ghys conjecture, where people set the problem and judged the output.

Three proofs and a Lean check

Two other proofs appeared within days. On 4 October, Pierre Bizeul, Boaz Klartag and Joseph Lehec posted a 32-page proof that calls the criterion from Song and Zhang's first version "the crucial step." Their acknowledgements go further than Microsoft's on the AI question: "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."

On 6 October, Krishnakumar Balasubramanian and Shiva Kasiviswanathan posted a third proof with an explicit bound: a Poincaré constant of at most 25 for every isotropic log-concave measure. They also say they had "substantial assistance from several frontier AI models" and verified the arguments themselves.

On 8 October a public repository, KLS500, appeared on GitHub describing itself as a Lean 4 formalization of KLS with a dimension-free Poincaré constant of at most 500. Microsoft's post cites a Lean formalization that combines the key criterion with other research. A project site run by Nicolas Brosse, The KLS theorem and its methods, now compares all three arguments, with its own steps checked by AI reviewer agents and, it says, not yet by any person. Lean is the same proof checker behind recent formal-verification work in AI-assisted mathematics.

What it does not show

None of the three papers has been through journal peer review yet, and the constants differ: the explicit ones are 25 in one preprint and 500 in the Lean repository, while Song and Zhang prove only that some universal constant exists. Agreement between independent proofs is strong evidence, but experts will still read the arguments line by line, as they did when an OpenAI Navier-Stokes claim turned out not to match its Lean code.

The result also does not show that AI systems can do research mathematics on their own. By Microsoft's account, the unguided runs failed. The Bizeul, Klartag and Lehec note suggests the share of ideas found by models varies a lot from paper to paper, and authors describe it in their own words, so the accounts are hard to compare. Nothing here measures how much time the tools saved.

Why it matters

For mathematicians, a central problem in convex geometry and probability is now very likely closed, and results that leaned on it can drop the assumption. For AI, this is one of the clearest cases yet of a famous open problem falling with models doing much of the derivation work, and of several groups converging on it at once. That is the scenario funders have started to bet on, including the Simons Foundation programme backed by OpenAI and Anthropic, and the one that worries the mathematicians pledging not to work for AI firms.

Microsoft says the authors are simplifying the proof and extending the formal check so others can examine and build on it. The shortened, Lean-checked version they promise is the next thing to watch, along with what referees make of all three proofs.