Microsoft Research uses AI agents to prove the 31-year-old KLS conjecture Other

Microsoft Research has announced a mathematical proof of the Kannan-Lovasz-Simonovits (KLS) conjecture, a central problem in high-dimensional convex geometry formulated in 1995. Researchers Zhao Song and Xinzhi Zhang collaborated with AI agents to explore more than 100 mathematical directions while directing the overall proof strategy.

The KLS conjecture asks whether cutting a high-dimensional convex body with a flat hyperplane is almost as efficient as cutting it with any curved surface. KLS asserts that the best flat cut differs from the optimal arbitrary cut by at most a fixed universal constant, regardless of the number of dimensions. The result governs how rapidly random walks explore space and underpins algorithmic bounds in sampling, high-dimensional statistics, and convex optimization.

AI agents helped identify key inequality criteria, ran algebraic calculations, and verified intermediate steps. The human researchers formulated the recursive technique and error bounds that finalized the proof. Microsoft noted that automated attempts without human guidance failed to make headway under a similar token budget. Independent proofs and formalization in the Lean 4 proof assistant have also been established to support the finding.

What it is

• The KLS conjecture. A 1995 open problem proposed by Ravi Kannan, Laszlo Lovasz, and Miklos Simonovits concerning isoperimetric bounds on convex bodies.
• Human-agent collaboration. AI agents explored over 100 candidate proof directions and handled verification, while human mathematicians directed the search and developed the core recursive framework.
• Lean 4 formalization. Microsoft confirmed the mathematical arguments are supported by separate proofs and machine verification in Lean 4.

Sources

• Microsoft Research announcement