Microsoft researchers resolve the 31-year-old KLS conjecture with human-directed AI agents; independent experts post a parallel proof calling their criterion the crucial step

Why it matters

【Key points】

Microsoft Research said on Oct 21 that Xinzhi Zhang and Zhao Song proved the 1995 Kannan–Lovász–Simonovits (KLS) conjecture using human-directed AI agents.

1. KLS asks whether, for log-concave distributions, the best flat cut is within a dimension-free constant of the best cut of any shape — central to high-dimensional sampling and optimization. The best prior bound (July 2026) still grew with dimension.

2. Agents explored ~100 research trajectories in parallel while researchers pruned them, yielding a new criterion. The Oct 1 paper reached an iterated-log bound; the Oct 4 version repeated the recursion and bounded the accumulated error, removing dimension dependence.

3. Unguided attempts with leading models on a similar token budget failed.

4. Bizeul, Klartag and Lehec posted an independent proof the same day, calling the Song–Zhang criterion "the crucial step"; a third proof and a Lean 4 formalization followed.

【Verifiable】

https://www.microsoft.com/en-us/research/blog/solving-a-31-year-old-grand-challenge-in-mathematics-the-kls-conjecture/

https://arxiv.org/abs/2610.01447

https://arxiv.org/abs/2610.05474

【Our read】

1. Background: most AI-math headlines involve contest problems or small improvements. KLS is a central open problem, backed here by independent proofs and formal verification — one of the strongest cases yet of AI helping settle a major question.

2. Comparison: unlike end-to-end model attempts or automated search like AlphaEvolve, humans did the pruning. The failed unguided control suggests research taste, not compute, is the bottleneck.

3. Impact: results that assumed KLS now hold unconditionally, and parallel agent exploration with expert pruning may become a standard workflow.

4. Caveat: models used are not named; journal review and the authors' full Lean release are pending.