Human-Directed AI Helps Microsoft Researchers Prove the 31-Year-Old KLS Conjecture

On October 21, 2026, Microsoft Research announced that senior researcher Xinzhi Zhang and co-author Zhao Song have proved the Kannan–Lovász–Simonovits (KLS) conjecture, a problem in high-dimensional geometry and probability that had been open since 1995.

What KLS says

KLS asks whether, for a broad class of high-dimensional probability distributions (log-concave ones), the best flat cut is always nearly as good as the best cut of any shape at finding the distribution’s narrowest bottleneck. The conjecture predicts the two differ by at most a universal constant, no matter how many dimensions there are. Because these bottlenecks govern how fast random walks can explore a distribution, KLS sits at the heart of the theory of high-dimensional sampling, optimization, and statistics.

Before this work, the best known result, from July 2026, still let the bound grow slowly with the dimension.

How AI helped

The authors used a human-directed agentic process: several AI agents explored variations of an idea in parallel, a researcher reviewed their intermediate results, pruned unpromising directions, and passed the best one to the next round. Microsoft says they explored more than 100 candidate approaches before finding a new criterion that became the foundation of the proof. AI tools also helped with derivations, the manuscript, and internal proof checks.

The researchers say the recursive method, its repeated application, and the proof that the errors stay bounded are their own contributions. In a separate test, repeated unguided attempts by several leading AI models, using roughly the same total token budget, fell short.

Independent confirmation

On the same day the complete proof was posted, mathematicians Pierre Bizeul, Boaz Klartag, and Joseph Lehec posted their own proof on arXiv, calling Song and Zhang’s criterion “the crucial step.” A third, related proof appeared the same day, and a Lean 4 machine-checked formalization followed. The authors say they’ve also verified a shortened version of their proof in Lean and plan to release it after final review.