KLS conjecture proved after 31 years, with AI agents under human guidance

What's happening

Microsoft Research reports that the Kannan-Lovász-Simonovits conjecture (KLS conjecture) has been proved. It was posed in 1995 and is considered one of the central open questions in high-dimensional geometry. The proof comes from two researchers, including Xinzhi Zhang from the Machine Learning and Optimization group at Microsoft Research. The blog post also names Zhao Song as a co-author. What stands out is how they got there: AI agents explored mathematical possibilities while the researchers evaluated the results, weeded out dead ends and redirected the search.

What the conjecture is about

The KLS conjecture concerns so-called log-concave distributions. This is a broad class of probability distributions in many dimensions, which includes, for example, the uniform distribution inside a convex body. You can picture such a distribution as a mass that you split into two parts with a cut. The question is where the narrowest "bottleneck" lies, that is, where the mass is hardest to divide.

The conjecture says it's enough to consider only flat cuts (hyperplanes). The best flat cut is worse than the best cut of any shape by at most a fixed, universal constant, regardless of how many dimensions the space has.

This matters in practice because the geometry of these cuts determines how quickly random walks explore a distribution. Such methods are used for sampling, that is, drawing samples from high-dimensional distributions. KLS therefore plays a role in statistics, optimization, algorithms and theoretical computer science. The MSRI institute called it a "central open problem of high-dimensional convex geometry," and the Simons Institute described it as one of the most important open problems in convex geometry.

The road to the proof

The starting point was a result from July 2026, in which the bound still grew slowly with the dimension. The authors first wanted to improve it and make the bound sharper. To do so, they worked with AI agents in a structured, human-guided process and examined more than 100 solution approaches, many involving long calculations with higher-order tensors (multidimensional generalizations of matrices). This produced a new mathematical criterion that forms the basis of the proof.

Then it turned out that this criterion can be applied recursively: each improved bound can be fed back into the same argument and yields an even better one. In the October 1, 2026 version, this reduced the dependence on dimension to the iterated logarithm. This function grows extremely slowly, but it does grow, so the conjecture was not yet fully proved.

The final step was to repeat the entire recursive refinement rather than apply it just once. The idea comes from the authors' earlier work on fast algorithms for linear programming. They proved that the small errors at each stage shrink fast enough that their sum stays bounded by a universal constant. That removed the dimension dependence, and the proof was complete in the October 4, 2026 version.

The role of AI

According to Microsoft, the recursive method, its repeated application and the proof that the errors stay bounded are the researchers' own contributions. AI tools helped explore approaches, carry out detailed derivations, prepare the manuscript and run internal proof checks. The researchers set the direction, picked promising ideas, assembled them into the proof and verified it.

They describe the process as an agentic search with step-by-step "pruning": several agents investigated variants of an idea in parallel, the researchers reviewed intermediate results, discarded unpromising directions and passed the best results on to the next round. Around a hundred research paths were pursued before the breakthrough came.

In a separate experiment, the authors repeatedly had several leading AI models work on the same problem without guidance, using roughly the same token budget. That failed. Microsoft concludes that the success depended on both the AI's capabilities and the researchers' mathematical judgment.

Independent confirmation

On the day the authors published their complete proof, a separate group of leading experts put a parallel, complete proof online. It builds on the first version of the Microsoft paper, whose criterion the group calls "the decisive step in the proof." A third proof, published the same day, relies on a closely related idea. A Lean 4 formalization (a machine-checkable proof) followed later, combining the key criterion from the first Microsoft paper with other work. The authors have also shortened their proof and verified the shorter version in Lean; both are expected to be released after final review.

Our take

If the proof holds, a number of results that previously assumed KLS now hold unconditionally. That strengthens the foundations of convex geometry, probability theory and theoretical computer science. The parallel proofs and the formalization suggest this is a real principle and not a fragile argument.

Caution is warranted on the AI side: the claims about unguided models failing come from Microsoft itself and haven't been independently verified, and the post doesn't say which models were used. The vendor's message is that guided human-AI collaboration amplifies human insight rather than replacing it. The result itself should stand regardless of that interpretation, because it can be checked mathematically.