The KLS proof is supported by a paper, parallel proofs and a Lean 4 formalization; the AI contribution was a human-directed multi-trajectory search.
Researchers prove the KLS conjecture with human-directed AI search
2026-10-04Verified announcementWATCH
Researchers proved the 31-year-old Kannan–Lovász–Simonovits conjecture, removing a dimension-dependent bound in high-dimensional sampling theory. The Microsoft-affiliated proof used a human-directed search across roughly 100 agent trajectories; two parallel proofs and a later Lean 4 formalization provide separate checks on the mathematics. The workflow result is retrospective evidence, not proof that an unguided model can solve comparable problems.
What this means for you
For teams building research agents, the result is unusually strong evidence for a workflow that combines broad machine search, human pruning and formal verification. It argues for exposing intermediate trajectories and proof obligations instead of measuring only final answers.
Evidence & related material
Technical details & scores
| Result | complete proof of the KLS conjecture with a dimension-free bound |
|---|---|
| Workflow | roughly 100 AI research trajectories with iterative human pruning |
| Independent Checks | two parallel proofs posted the same day; later Lean 4 formalization |
| Limit | unguided runs at the same token budget did not find the proof, according to Microsoft |
| Time Basis | proof paper first posted 2026-10-04; official retrospective published 2026-10-21T16:00:00Z |
Technical impact 5
Engineering value 3
Adoption signal 2
Maturity 2
Verification cost 4
Risk 2