Researchers from Microsoft Research have proven the Kannan-Lovasz-Simonovits (KLS) conjecture, a 31-year-old problem in high-dimensional geometry. The team, consisting of Zhao Song and Xinzhi Zhang, utilized AI agents to explore over 100 potential solution paths and verify intermediate mathematical reasoning.
The KLS conjecture addresses the geometry of high-dimensional convex bodies and the efficiency of partitioning them. It posits that the difference between the best flat cut and an optimal arbitrary cut is bounded by a constant, independent of the number of dimensions. This property is critical for random sampling algorithms in statistics and computer science.
The AI agents assisted the researchers by performing complex tensor calculations and testing various mathematical criteria. The team employed an iterative process where multiple agents explored different directions, while the scientists evaluated results and discarded ineffective approaches to focus on the most promising ones.
The final proof relies on a recursive application of a newly discovered criterion. By refining estimates iteratively, the researchers demonstrated that errors remain bounded regardless of dimensionality. The proof has been formalized in the Lean 4 system to ensure mathematical rigor and was supported by independent findings.
