Proofs of the KLS conjecture appear
On 4 October 2026 Zhao Song and Xinzhi Zhang (the latter of Microsoft Research) posted version 2 of an arXiv preprint that, by the authors' account, gives a dimension-free bound on the KLS constant and settles the 31-year-old Kannan–Lovász–Simonovits conjecture on cuts of high-dimensional distributions. The same day Pierre Bizeul, Boaz Klartag and Joseph Lehec posted their own proof, built on the criterion from the first version. Microsoft's post of 21 October says AI agents under human direction found that criterion.
Why it matters
If the proofs hold, a bound that grew slowly with dimension becomes a constant, and results that assumed the conjecture become unconditional. Two things set the case apart from the month's other AI-assisted claims: a separate group of specialists independently wrote a proof from the first paper's criterion, and the authors say AI searched for approaches while people assembled and checked the argument. These are the authors' words, not a reviewers' verdict.
What the pages say. arXiv 2610.01447 (Song, Zhang): version 1 of 1 October 2026 (10:43 UTC) had a bound of O(4^(log* n)) against a previous best of log^(1/4) n credited to Letwin (the post dates the best previous result to July 2026); version 2 of 4 October (21:21 UTC), 140 pages, gives ψ_n ≤ C for a universal constant C and a similar bound for the Poincaré constant. arXiv 2610.05474 (Bizeul, Klartag, Lehec), version 1 of 4 October (19:30 UTC), 32 pages, comment: "contains a paragraph describing AI use"; its abstract calls the criterion of Song and Zhang "the crucial step". Microsoft Research's post of 21 October (16:00 UTC) describes the search: about a hundred trajectories explored in parallel by agents while a person pruned unpromising directions; an attempt on the same problem without such guidance, with several leading models and roughly the same token budget, "fell short". The post says a third proof appeared the same day; arXiv's page for it (2610.07728, Balasubramanian and Kasiviswanathan) shows version 1 on 6 October. The post calls a Lean 4 formalisation later: the GitHub repository HongruZhao/KLS500 (created 8 October 2026, 04:01 UTC) rests chiefly on the Bizeul–Klartag–Lehec route, says 1,710 modules were rebuilt and notes that Comparator and Nanoda were not run. What the record does not claim. The proofs were not checked here: the word "settled" belongs to the authors and the independent group, not to the Atlas. The Lean repository is a third party's work, not Microsoft's, and was not reviewed. Microsoft's post is the account of one author's employer. The record is dated 4 October, the day of the complete proof; the post of 21 October is a report on it.