AI agents help Microsoft Research prove the 31-year-old KLS geometry conjecture
Microsoft Research researcher Xinzhi Zhang and independent researcher Zhao Song used AI agents to map out math approaches, but human oversight drove the proof.
Microsoft Research researcher Xinzhi Zhang and independent researcher Zhao Song have presented a proof for the Kannan–Lovász–Simonovits (KLS) conjecture, formulated in 1995. The problem sits in high-dimensional geometry and governs how efficiently random algorithms explore complex spaces.
Stated simply, the conjecture posits that for a specific class of multidimensional distributions, a flat cut can estimate the narrowest bottleneck of a space within a constant factor that does not grow with the number of dimensions. This geometry dictates the mixing speed of random walks used in sampling and optimization. The new proof removes an extra assumption from multiple theoretical frameworks that previously relied on the conjecture.
To tackle it, the researchers tested over 100 possible approaches, requiring heavy high-order tensor computations. This work yielded a new mathematical criterion that formed the core of the proof. Researchers then applied a recursive refinement method, using one step's result to improve the next. The crucial final step involved reapplying the entire procedure while proving that accumulated errors remain bounded by a constant regardless of spatial dimension.
AI agents handled parallel searches, calculations, and intermediate reasoning checks. However, human scientists evaluated intermediate results, filtered out weak ideas, and directed the search. In separate experiments, leading models attempted to solve the problem without human guidance using a comparable token budget and failed.
The work surfaced on arXiv in early October, with Microsoft Research detailing it on October 21. On that same day, another group of mathematicians released a separate proof calling Zhao Song and Xinzhi Zhang's new criterion a key step toward the solution, alongside a third proof built on a similar idea. Formalization in Lean 4 has begun, with authors noting they verified a shortened version of their proof and are preparing it for publication.
Source: Microsoft Research blog
Source: arXiv preprint 2610.01447
Source: habr
Comments
Help shape the next version: Add context or suggest a correction. AI review can add points toward a rewrite. Reviews and updates may take time; a full meter does not guarantee a new version.