KLS conjecture proof: three papers claim the 31-year-old problem, and what AI did in each

A KLS conjecture proof, settling a 1995 problem in high-dimensional geometry, was posted to arXiv in early October 2026, and AI played a documented part. On October 21, 2026, Microsoft Research said its researcher Xinzhi Zhang and co-author Zhao Song had proved the Kannan–Lovász–Simonovits conjecture with a "human-directed agentic research process," without naming the AI models. A separate paper posted October 4 by Pierre Bizeul, Boaz Klartag and Joseph Lehec goes further, saying most of its proofs "were found by ChatGPT." It's the latest test of what reasoning models can contribute to research mathematics. None of the papers has been peer reviewed.

This story is based on the three arXiv papers, Microsoft Research's October 21 blog post and the public Lean formalization, checked October 22 and 23, 2026. For how a machine proof checker changes the trust question, see our explainer on OpenAI's Navier–Stokes claim.

The short version

• The problem: the KLS conjecture says that in any high-dimensional convex shape (and a wider family of "log-concave" distributions), the best straight cut is nearly as good as the best cut of any shape, up to a universal constant.
• Who: Zhang (Microsoft Research) and Song (independent researcher); Bizeul, Klartag and Lehec; and, separately, Krishnakumar Balasubramanian and Shiva Kasiviswanathan.
• AI's role: Microsoft describes AI agents exploring more than 100 approaches under human direction. The Bizeul–Klartag–Lehec paper credits ChatGPT with most of its proofs. The third paper's abstract doesn't mention AI.
• Checked how: a Lean 4 formalization is public on GitHub. Formal peer review hasn't happened yet.

What is the KLS conjecture?

Picture a convex shape, with no dents or holes, in thousands of dimensions, which you want to cut in two with the smallest possible cut surface. Microsoft's post frames the question as whether "the best flat or hyperplane cut is always nearly as effective as the best cut of any shape." The conjecture says yes: the gap is bounded by a constant that doesn't grow with the number of dimensions.

Microsoft notes that this geometry controls how fast random walks explore a distribution, so KLS bears on sampling algorithms. Before October, the best result let the bound grow slowly with dimension: Brayden Letwin's July 2026 bound of order log^(1/4) n, which Song and Zhang cite as the result they improved.

Who proved it, and when?

How the KLS proofs appeared on arXiv

1. Oct. 1, 2026Song and Zhang post a near-constant bound and a new criterionarXiv 2610.01447Confirmed
2. Oct. 4, 2026Song and Zhang's revised version completes the proofarXiv 2610.01447v2; Microsoft ResearchConfirmed
3. Oct. 4, 2026Bizeul, Klartag and Lehec post a full proofarXiv 2610.05474Confirmed
4. Oct. 6, 2026Balasubramanian and Kasiviswanathan post a proof with an explicit boundarXiv 2610.07728Confirmed
5. Oct. 21, 2026Microsoft Research announces the resultMicrosoft ResearchConfirmed

Song and Zhang's first version, posted October 1, 2026, didn't finish the job. It cut the bound to one that grows with the iterated logarithm of the dimension, which barely grows at all, and introduced a new criterion. Microsoft says the authors "completed the proof in the October 4, 2026 version of the paper," and arXiv's listing dates that second version October 4. The current PDF is titled "An O(1) Bound for the KLS Constant."

On the same day, Microsoft says, "a separate group of experts posted a full proof," developed in parallel and built on the first Song–Zhang version. That's the Bizeul–Klartag–Lehec paper, "Presenting a proof of the Kannan-Lovász-Simonovits conjecture," whose abstract calls the Song–Zhang criterion "the crucial step in the proof."

Microsoft also mentions a third proof that "appeared separately on the same day" and "relies on a closely related idea," without naming it. A third dimension-free proof on arXiv, by Balasubramanian and Kasiviswanathan, was submitted October 6 and revised October 8. Its abstract describes a deterministic variational proof with an explicit bound of 25 on the Poincaré constant. It isn't clear whether this is the paper Microsoft means.

How exactly was AI used?

Microsoft's account. The post describes "agentic search with iterative human-assisted pruning." AI tools explored candidates, carried out detailed derivations, helped prepare the manuscript and ran internal proof checks. The researchers say they set the direction, chose the promising ideas, assembled the final argument and verified it. The post calls the recursive method and the error-bounding proof the researchers' original contributions. It also reports a control: "repeated unguided attempts to solve the same problem with several leading AI models," using about the same total token budget, "fell short of the goal." The models aren't named, so the comparison can't be checked.

Bizeul, Klartag and Lehec's account is unusually blunt. Their acknowledgments say: "Most proofs and mathematical ideas in this paper were found by ChatGPT; a notable exception is the idea to use suspension which was suggested by the authors. The role of the authors has been mostly to understand these proofs and improve their exposition." The paper opens by saying the conjecture "poses little challenge for contemporary AI tools, given the remarkable progress in our understanding of high-dimensional convex bodies in recent decades." It doesn't say which ChatGPT model or settings were used, or how the authors checked each AI-generated step beyond understanding it.

Has the proof been checked or peer reviewed?

Not by a journal. All three are arXiv preprints, and none says it has been submitted or accepted; as of October 23, 2026, none of their arXiv listings carries a journal reference.

There is machine checking. A public GitHub repository, KLS500, contains Lean 4 proofs of a dimension-free Poincaré bound with constant 500. Its README says it rests "chiefly on the cumulant and suspension approach" of Bizeul, Klartag and Lehec and also cites the Song–Zhang criterion and the Balasubramanian–Kasiviswanathan manuscript. It reports that the only axioms used are Lean's three standard ones, and notes that two further checkers "were not run." It doesn't name its author beyond the GitHub account HongruZhao, or say whether AI wrote the code. Microsoft says Zhang and Song separately verified "the streamlined argument in Lean" and plan to release it "after final review."

As our Navier–Stokes explainer notes, a Lean check proves the formal statement; the remaining risk is whether that statement matches the problem.

What do experts say?

Little so far. Microsoft's post quotes older descriptions of the problem, such as the Simons Institute's "one of the most important open problems in convex geometry." No Quanta article on the October proofs, and no comment from independent mathematicians in a major outlet, had appeared by October 23, 2026. Klartag and Lehec, whose earlier bounds the new work supersedes, are co-authors of one of the proofs.

For how model "thinking" produces long derivations, see our reasoning models explainer; for another AI-assisted research result that humans checked, see how Claude traced the NIST curve seeds.

What's confirmed, reported and uncertain

• Confirmed: the three arXiv papers, their authors and dates; the Bizeul–Klartag–Lehec ChatGPT acknowledgment; Microsoft's description of its process; the public KLS500 Lean repository.
• Company-reported: that unguided AI attempts fell short; that the recursive method was the researchers' own; the Song–Zhang Lean check, not yet released.
• Uncertain: which AI models Microsoft's team used; which ChatGPT model Bizeul, Klartag and Lehec used; peer review; whether the third proof uses AI.