Microsoft details how human-guided AI helped solve a 31-year-old math problem

Microsoft Research on October 21 described how human-directed AI helped resolve a 31-year-old geometry problem underpinning the study of randomized algorithms. Its account credits researchers with choosing the mathematical direction and assembling the proof—not simply handing the problem to an autonomous system. The completed argument appeared on October 4.

The researchers, Microsoft’s Xinzhi Zhang and collaborator Zhao Song, report proving the Kannan–Lovász–Simonovits conjecture, known as KLS. Proposed in 1995, it concerns how geometry creates bottlenecks in high-dimensional probability distributions. Those bottlenecks help determine how quickly random walks can explore a distribution.

Researchers chose which paths survived

The project began by trying to sharpen the best previously known bound, established in July 2026. That result still allowed the bound to grow slowly as the number of dimensions increased. Zhang and Song sought a more precise mathematical criterion that could improve it.

According to the researchers, multiple AI agents explored variations of ideas in parallel. Humans examined intermediate results, discarded unpromising directions and passed the strongest results into the next round. The search covered more than 100 candidate approaches, many involving lengthy calculations with higher-order tensors.

AI tools also assisted with detailed derivations, manuscript preparation and internal proof checks. The researchers retained responsibility for selecting ideas, connecting them into the final argument and verifying the proof. Microsoft attributes the recursive method and the argument controlling its accumulated errors to the researchers.

October’s two-step finish

KLS asks whether a simple flat cut can capture a distribution’s narrowest bottleneck nearly as well as a cut of any shape. For the class of distributions called log-concave distributions, the conjecture predicts that the two differ by at most a fixed factor, regardless of dimension.

The new criterion supplied a way to feed an improved bound back into the same argument and obtain a tighter one. In the October 1 version of the paper, this reduced the remaining dimension dependence to the iterated logarithm: a function that grows extraordinarily slowly, but still grows.

The final step repeated the entire recursive refinement, drawing inspiration from the authors’ earlier work on fast linear-programming algorithms. They showed that small errors introduced along the way shrink quickly enough for their total to remain bounded. The October 4 version thereby removed dependence on dimension altogether.

Other proofs and a machine-checked argument

A separate paper by Pierre Bizeul, Boaz Klartag and Joseph Lehec, submitted October 4, also presents a proof. Its abstract identifies Song and Zhang’s criterion as the crucial step. That is confirmation of the criterion’s mathematical importance, while making clear that the other proof builds on it.

Microsoft says a third proof appeared that day using a closely related idea. A subsequent Lean 4 formalization—a machine-checked mathematical argument—combined the initial criterion with additional research. These checks concern the mathematics; the comparison between guided and unguided AI remains the researchers’ account of their own project.

The payoff Microsoft describes is foundational: results that previously assumed KLS can now be stated without that assumption. The authors have also shortened their proof and say they verified the streamlined argument in Lean. They plan to release both after final review, giving the field another version to examine and build upon.