Microsoft Says AI-Aided Proof Settles KLS Conjecture

A problem in high-dimensional geometry that has been open since 1995 has been solved, Microsoft Research says, with researchers steering AI agents rather than handing the problem to a single model. The claim rests on a preprint posted to arXiv by Xinzhi Zhang of Microsoft Research and Zhao Song. It has not been peer reviewed.

The Kannan–Lovász–Simonovits (KLS) conjecture asks whether, for a broad class of high-dimensional probability distributions, the best flat cut through a shape is always nearly as good as the best cut of any shape, within a fixed factor no matter how many dimensions there are. It matters because the geometry of those cuts governs how quickly random walks can explore a distribution, which underpins sampling, volume computation and parts of convex optimisation. Microsoft quotes the Simons Institute calling it “one of the most important open problems in convex geometry”.

From a slowly growing bound to a constant

The proof came in two steps, according to Microsoft’s blog post. Starting from a July 2026 result whose bound still grew slowly with dimension, the authors found a new criterion and applied it recursively. The 1 October version of their paper cut the dependence on dimension to an iterated logarithm, which grows extraordinarily slowly but still grows. The 4 October version repeated the whole recursive refinement and showed that the errors added at each stage stay bounded by a universal constant, completing the proof.

Microsoft is explicit about who did what. AI tools “helped explore candidate approaches, carry out detailed derivations, prepare the manuscript, and perform internal proof checks”, it says. The researchers “determined the mathematical direction, selected the promising ideas, assembled them into the final argument, and verified the proof”. Microsoft says the recursive method, its repetition and the proof that accumulated errors stay bounded are the researchers’ own contributions. It does not name the models it used.

A hundred trajectories, and a control run that failed

The working method was a kind of supervised search. Several agents explored variations of an idea in parallel; a researcher examined the intermediate results, cut off unpromising lines and passed the best one to the next round. The team explored “more than 100 candidate approaches”, and “roughly one hundred research trajectories were explored before the key breakthrough emerged”, Microsoft says.

The company also ran a comparison. In a separate track, the authors made repeated unguided attempts at the same problem with several leading AI models, using roughly the same total token budget. “That effort fell short of the goal,” Microsoft says. Microsoft says success depended on both the AI systems and the researchers’ judgement. The control run is its evidence that direction mattered, though it is a single, self-reported comparison.

Other mathematicians reached the same place

The result is not resting on one paper alone. On 4 October, Pierre Bizeul, Boaz Klartag and Joseph Lehec posted their own proof, developed in parallel. Their abstract says “the crucial step in the proof is the very recent criterion from Song and Zhang”. Their acknowledgements add a twist of their own: “Most proofs and mathematical ideas in this paper were found by ChatGPT,” with the exception of one idea the authors supplied.

Microsoft also points to a third proof and to a Lean 4 formalisation. Hongru Zhao, who describes building that formalisation with Codex in about 24 hours, says it mainly follows the Bizeul–Klartag–Lehec route using Song and Zhang’s comparison. He is careful to call his audits “local checks by the proof system and checking agents, not an external mathematical review”. Zhang and Song say they have shortened their own proof and checked it in Lean, and plan to release both after final review.

Microsoft argues that independent proofs are “among mathematics’ strongest forms of validation”. Journal review of the papers is still to come. TSN reported last week on new funding from the Simons Foundation, Anthropic and OpenAI for AI maths work. The KLS papers give that field a high-profile test case, with the credit split between people and machines spelt out unusually plainly.