Microsoft Research’s illustration of the KLS conjecture: a flat cut through a tetrahedron beside the smallest curved cut. Image: Image: Microsoft
A geometry problem that has beaten mathematicians since 1995 may finally be solved, and the two researchers behind the proof say a team of AI agents did much of the legwork. Microsoft Research senior researcher Xinzhi Zhang said on Wednesday that she and Zhao Song, listed on the paper as an independent researcher, have proved the Kannan-Lovász-Simonovits (KLS) conjecture in a 140-page paper on arXiv.
It has not been peer reviewed, but it has passed a tough informal test: within days, a rival team including Boaz Klartag, who set some of the earlier records on the problem, posted a proof built on it.
What the KLS conjecture says #
Ravi Kannan, László Lovász and Miklós Simonovits posed the conjecture in 1995. It concerns convex shapes and “log-concave” probability distributions in any number of dimensions. Roughly, it says the cheapest way to cut such a shape into two large pieces is never much better than the best flat cut, by a factor that stays fixed however many dimensions you add.
The geometry of cuts controls how quickly a random walk can explore a shape, so the conjecture sits under algorithms for sampling, computing volumes and convex optimisation. The Simons Institute has called it “one of the most important open problems in convex geometry”.
Progress came in steps, through Ronen Eldan’s stochastic localisation method, Yin Tat Lee and Santosh Vempala, Yuansi Chen, and Klartag and Joseph Lehec, each shrinking how fast the bound grows with dimension. In July, Brayden Letwin set the latest record. The new paper claims a fixed constant: the conjecture itself.
A hundred approaches, pruned by people #
The paper’s AI disclosure says the push began on July 28, the day after Letwin’s preprint. The authors explored “more than 100 approaches in collaboration with AI tools”, generated together, “with the authors deciding which ones to prioritize”. Zhang’s post describes agents trying variations in parallel while a researcher pruned dead ends and fed the best result into the next round. AI also did derivations, manuscript preparation and internal proof checks.
The paper names the tools: OpenAI’s GPT-6 Astra and GPT-5.6 Sol, and Anthropic’s Claude Fable 5 and Fable 5.1. The step that finished the job, repeating a refinement until the errors shrink fast enough to stay bounded, was the researchers’ own, both say. Zhang also wrote that unguided attempts with several leading models, on roughly the same token budget, fell short, and that “the eventual success depended on both the capabilities of the AI systems and the mathematical judgment of the researchers”.
The paper closes on who answers for it:
All of the proofs have been carefully verified by the authors and several AI tools. The authors take full responsibility for the correctness of the proofs.
Zhao Song and Xinzhi Zhang, in their paper
Three proofs in a week, and a Lean check #
On October 4, the day Song and Zhang posted their complete proof, Pierre Bizeul and Boaz Klartag of Israel’s Weizmann Institute and Joseph Lehec of Sorbonne University posted a 32-page proof of their own. Its abstract calls Song and Zhang’s criterion “the crucial step in the proof”. Its acknowledgements are blunter still about the machines:
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.
Pierre Bizeul, Boaz Klartag and Joseph Lehec, in their paper
A third proof, by Krishnakumar Balasubramanian and Shiva Kasiviswanathan, followed on October 6 and claims an explicit constant of 25 for the closely related Poincaré inequality. A Lean 4 formalisation on GitHub, built mainly on the Bizeul, Klartag and Lehec route, says it machine-checks the result. Zhang says the Microsoft pair have checked a shorter version of their own proof in Lean and will release it after a final review.
Not peer reviewed yet #
None of the three papers has been through journal review, and MadRobot found no published assessment yet from mathematicians outside the teams involved. Still, independent proofs plus a machine-checked version are about as strong as early validation gets, a different picture from OpenAI’s batch of 722 AI-written maths papers, three of which it pulled a day later.
Mathematicians already say AI threatens their field but they can’t stop using it, and Fields medallists have asked labs to stop testing maths on models nobody else can use. Here the models are named, and anyone can pay for them.
Why it matters #
KLS is not a puzzle set to test AI: it is a 31-year-old problem that leading mathematicians spent years on, and if the proof holds, results that assumed it can now be stated without conditions. By the authors’ account, the machines did the searching and the people supplied the judgement and the final idea, a template other researchers will now try to copy.
Sources: Microsoft Research blog; Song and Zhang, An O(1) Bound for the KLS Constant (arXiv); Bizeul, Klartag and Lehec, Presenting a proof of the Kannan-Lovász-Simonovits conjecture (arXiv); Balasubramanian and Kasiviswanathan, A Dimension-Free Bound on the Poincaré Constant of Isotropic Log-Concave Measures (arXiv); Letwin, The KLS constant is O(log^1/4 n) (arXiv); KLS500 Lean formalisation (GitHub).