On October 21, 2026, Microsoft Research published “Solving a 31-year-old grand challenge in mathematics - the KLS conjecture”, describing how Xinzhi Zhang and co-author Zhao Song resolved the Kannan-Lovasz-Simonovits (KLS) conjecture, posed in 1995. The conjecture asks whether, for isotropic log-concave distributions in any dimension, the best flat cut through the distribution is always nearly as good as the best cut of any shape, with the gap bounded by a universal constant independent of dimension. It governs how fast random walks mix in high dimensions, which underlies sampling and volume-estimation algorithms.
The paper, “An O(1) Bound for the KLS Constant” (arXiv:2610.01447, 140 pages), was first posted on October 1, 2026, with a version 2 on October 4. According to the blog, the first version reduced the dimension dependence to an iterated logarithm and the second removed it entirely; the previous best result, from July 2026, still grew slowly with dimension.
Microsoft describes a “human-directed agentic research process”: multiple AI agents explored more than 100 candidate approaches in parallel while the researchers pruned and redirected the search, and the AI tools helped with derivations, manuscript preparation and internal proof checks. The researchers say they set the direction, selected ideas and verified the final proof, and that repeated unguided attempts with several leading AI models fell short. A separate group posted a full proof the same day building on the first version (arXiv:2610.05474), a third proof uses a closely related idea, and a Lean 4 formalization has been released on GitHub.
Why it matters: KLS is one of the central open problems of high-dimensional geometry and probability, and its resolution is a prominent case of AI agents materially contributing to a frontier mathematical result, with independent proofs and machine-checked formalization following within weeks.
What it does not show: the blog does not name the AI models used or which steps they contributed, the result has not yet been through journal peer review, and it remains unclear from the post how much of the original argument the released Lean formalization covers. The underlying paper predates this announcement by about three weeks.