Solving a 31-year-old grand challenge in mathematics – the KLS conjecture microsoft.com

Microsoft Research’s Xinzhi Zhang, Zhao Song and collaborators say they have proved the 1995 Kannan–Lovász–Simonovits conjecture, showing that for log-concave distributions the best flat cut is within a dimension-independent constant of the best cut of any shape. The proof used human-directed AI exploration; separate researchers produced parallel proofs, and a Lean formalization provides additional verification.