Microsoft Research proves the 31-year-old unsolved KLS conjecture

Microsoft Research researcher Xinzhi Zhang and co-authors proved the KLS conjecture proposed in 1995, giving a dimension-independent fixed bound; the previous best result only allowed the bound to grow slowly with dimension. The proof came from a human-guided agent search process, in which the team explored more than 100 candidate paths, with researchers evaluating, pruning, and redirecting them; an independent team also gave a complete proof at the same time, followed by Lean 4 formal verification. The authors say earlier unguided end-to-end attempts with multiple frontier models failed to achieve the goal.