Microsoft researchers say AI agents helped resolve the 31-year-old KLS conjecture

Microsoft Research published a blog post saying that Xinzhi Zhang, a researcher in its Machine Learning and Optimization group, and a collaborator, Zhao Song, had proved the Kannan–Lovász–Simonovits (KLS) conjecture using a human-directed process in which AI agents explored mathematical approaches. The post is dated 21 October; the proof itself was on arXiv earlier.

The conjecture, proposed in 1995, concerns high-dimensional probability distributions of a broad type. It asks whether the best flat cut through such a distribution is within a universal constant of the best cut of any shape, whatever the dimension. It governs how quickly random walks explore these distributions, and so bears on sampling and volume-computation algorithms. According to the post, the best earlier result, from July 2026, allowed the bound to grow slowly with dimension.

The paper, “An O(1) Bound for the KLS Constant”, was first submitted on 1 October and revised on 4 October. Microsoft says the first version reduced the dimension dependence to an iterated logarithm and the 4 October version removed it. The authors say AI helped explore candidate approaches, carry out derivations, draft the manuscript and run internal checks, while they chose the direction and verified the proof. The post describes agents working in parallel with a researcher pruning weak directions between rounds, roughly one hundred trajectories before the key step, and separate unguided attempts with “several leading AI models”, on a similar token budget, that failed. It does not name the systems. The arXiv paper itself does not mention AI use.

Microsoft’s post says multiple independent researchers have validated the work. A separate proof by Pierre Bizeul, Boaz Klartag and Joseph Lehec was posted on 4 October and describes Song and Zhang’s criterion as “the crucial step”. That paper therefore confirms the proof’s route rather than reaching it independently. A third preprint followed on 6 October, and, Microsoft says, a Lean 4 formalisation was subsequently released. It adds that its own shortened proof and Lean verification are still to be released after review. The post comes from the authors’ employer, and the claim about AI’s role rests on their account.

It follows OpenAI’s October publication of AI-written proofs and its Navier–Stokes claim. Here the reported role of the AI was narrower: exploration and checking under a mathematician’s direction, which the post contrasts with asking a model to solve the problem in a single run.