KLS conjecture resolved with human-directed AI exploration
Microsoft Research announced on 21 October 2026 that Xinzhi Zhang, a senior researcher in its Machine Learning and Optimization group, and the independent researcher Zhao Song had proved the Kannan-Lovasz-Simonovits conjecture, posed in 1995. Their 140-page paper, "An O(1) Bound for the KLS Constant", was posted to arXiv on 1 October and revised on 4 October; it shows that the KLS constant is bounded by a universal constant independent of dimension, establishing a dimension-free isoperimetric principle for isotropic log-concave measures. Microsoft described a human-directed agentic process begun on 28 July in which AI systems explored roughly 100 research trajectories while the authors chose which to pursue, with the models also carrying out derivations and internal proof checks; the paper names GPT-6 Astra, GPT-5.6 Sol, Claude Fable 5 and Claude Fable 5.1. Independent proofs by Pierre Bizeul, Boaz Klartag and Joseph Lehec appeared within days, and a Lean 4 formalisation was posted.
Why It Mattered
The KLS conjecture is a central question in high-dimensional geometry and probability, governing how fast random walks mix and therefore underpinning sampling algorithms used throughout statistics, optimisation and theoretical computer science. Its resolution would be a notable mathematical event regardless of method; what places it in a history of AI is the account of how the proof was assembled and how carefully that account was drawn. Microsoft's framing is deliberately narrow. The agents generated and tested candidate approaches at a rate no human team could match, but the researchers selected directions, judged which partial results were worth recursion and wrote the argument. Microsoft also reports that unguided attempts on the same problem failed. The Bizeul-Klartag-Lehec paper, produced in parallel, credits substantial assistance from a chatbot for parts of its own proofs. Within days there were three independent routes to the same theorem, all with models somewhere in the loop, and a machine-checked formalisation besides. That convergence is the significant datum. It suggests that the binding constraint on a class of open problems was search throughput over known techniques rather than a missing idea, and that the constraint has now loosened. It also gives mathematicians an unusually clean comparison between directed and undirected use of AI on the same target, at a moment when the discipline is contesting how machine contributions should be credited, verified and refereed. The near-simultaneous Lean formalisation points to the verification regime that is likely to follow: if proofs are produced faster than referees can read them, machine checking becomes the arbiter rather than a curiosity.
Who Built It
Zhao Song and Xinzhi Zhang (Microsoft Research)
Applications
- Mathematics
- High-Dimensional Geometry
- Sampling Algorithms