Researchers prove the KLS conjecture after 31 years

What the proof establishes

The conjecture asks whether a hyperplane can cut a broad class of high-dimensional probability distributions nearly as effectively as an arbitrary-shaped boundary. For decades, evidence pointed toward yes, but no proof had established a bound independent of the number of dimensions.

The new proof does. It improves on the best earlier result, published in July 2026, where the bound still grew slowly with dimension. A version of the paper dated October 1, 2026, reduced that dependence to an iterated logarithm: an exceptionally slow-growing function, but one that still grows. The October 4, 2026, version removes the dependence entirely.

The significance was clear well before the proof. The Mathematical Sciences Research Institute called the conjecture one of the central open problems in high-dimensional convex geometry in its 2017–2018 annual report. The Simons Institute described it as one of the most important open problems in the field. At the 2022 International Congress of Mathematicians, Ronen Eldan highlighted its reach across high-dimensional convex geometry and computational geometry; Quanta described it as underlying many questions in statistics and computer science.

Figure 1: An illustration of the KLS Conjecture (simplified) on regular tetrahedron.

Source: microsoft.com

A search, then a recursive argument

The researchers first improved the July 2026 bound. AI agents took part in a structured search through more than 100 possible approaches, many involving lengthy computations with higher-order tensors. That exploration led to a new mathematical criterion, which became the basis of the proof.

The crucial move was to apply the criterion recursively: feed each improved bound back into the same argument to get a better one. The final proof repeats that refinement and shows that the small errors introduced at each stage shrink quickly enough for their total to remain bounded by a universal constant.

The recursive method, its repeated application and the proof that the accumulated errors stay bounded are the researchers’ original results. AI tools helped explore approaches, work through detailed derivations, prepare the manuscript and conduct internal checks. The researchers chose the mathematical direction, selected promising ideas and assembled and checked the final argument.

Independent checks, with a caveat

On the day the full proof appeared, another group of leading researchers published a version developed in parallel, using results from the first Microsoft paper that its authors described as a key step. A third proof based on a related idea appeared separately the same day. A Lean 4 formalization followed, combining the main criterion from the first Microsoft paper with results from other work.

Independent proofs are particularly persuasive in mathematics because they show that a result does not rest on a single chain of reasoning. The authors also shortened their proof and checked a simplified version in Lean; they plan to release both versions after a final review.

I think the AI story here is narrower, and more useful, than a claim that a model solved a famous problem. The researchers also tried repeatedly to solve the same problem without their iterative human guidance, using several leading AI models. Those attempts received roughly as many tokens as the main process and did not succeed. The evidence points to a particular workflow: agents explored possibilities in parallel, while a researcher assessed intermediate results, discarded weak directions and chose what to pursue next. The paper does not show that autonomous agents can carry out mathematical research on their own.

The proof removes a hypothesis that many earlier results relied on, allowing them to be stated without that assumption. But the work also leaves a practical task: its authors are still simplifying the argument and extending its formal verification so other mathematicians and theoretical computer scientists can more easily inspect and build on it. A theorem can settle a conjecture; making its proof usable is the next test.