Microsoft Solves a 31-Year-Old Math Problem Using AI Agents

Researchers at Microsoft Research, working with a collaborator, have announced a proof of the Kannan-Lovász-Simonovits conjecture. The 31-year-old problem asks whether a key geometric bound remains constant as dimension grows. The new argument removes the final dependence on dimension.

KLS governs bottlenecks in high-dimensional probability distributions, which in turn determine how quickly many random-walk algorithms converge. Analyses of Markov chain Monte Carlo, convex-body volume estimation, randomized optimization, and concentration inequalities can now invoke a theorem where they previously needed a conjecture. Existing implementations remain unchanged, and the proof does not yet provide a practical numerical constant.

• Claim: The KLS constant has a universal bound independent of dimension.
• Method: A self-improving argument is applied recursively until the remaining error is bounded.
• AI role: Human-directed agents explored more than 100 candidate research paths and assisted with calculations, drafting, and checks.
• Verification: Two additional proofs appeared, and a public Lean 4 formalization mechanically checks a related argument.

The geometry behind the runtime

The KLS conjecture concerns log-concave probability distributions, a broad family that includes Gaussian distributions and many convex optimization models. A distribution is log-concave when the logarithm of its density is concave, a property that rules out separated peaks and gives the distribution useful geometric structure.

After shifting and rescaling such a distribution into isotropic position, meaning zero mean and identity covariance, KLS compares two ways of partitioning its mass. One uses a hyperplane. The other may use any measurable boundary. The conjecture predicts that the best hyperplane cut is within a universal factor of the best unrestricted cut, regardless of the number of dimensions.

This comparison controls conductance, which measures how easily a random walk moves between regions of a distribution. A narrow bottleneck traps the walk and increases its mixing time, the number of steps required before its samples closely approximate the target distribution. KLS supplies a dimension-independent limit on that geometric obstruction.

Why dimension kept leaking in

Researchers had improved the KLS bound steadily since the conjecture was posed in 1995, but every proven estimate retained some dependence on the ambient dimension. The best result reported before this proof, established in July 2026, grew slowly with dimension. Any algorithmic theorem that imported the estimate also inherited that extra factor.

An October 1, 2026 version of the new work reduced the dependence to the iterated logarithm, written log*. This function counts how many times a logarithm must be applied before a value becomes small. It grows extraordinarily slowly, yet remains unbounded, so the draft stopped just short of proving the conjecture.

Recursion closes the gap

The paper organizes the proof around a criterion that improves an existing KLS estimate whenever one is supplied. The argument proceeds in three stages:

1. Strengthen the criterion. The authors derived a sharper inequality through calculations involving higher-order tensors and explored more than 100 candidate approaches.
2. Feed the result back. Each improved bound becomes the input to another application of the same criterion, producing a progressively tighter estimate.
3. Control the accumulated error. The authors proved that errors introduced during repeated applications shrink quickly enough for their total to remain bounded by a universal constant.

The third stage removes the residual log* term. Once the error series is shown to converge, the resulting KLS bound no longer grows with dimension.

How the agent search worked

The researchers used multiple AI agents inside a supervised search process rather than assigning the entire conjecture to a single system. According to their account, the workflow divided the work as follows:

• Agents explored variations of candidate ideas in parallel.
• Researchers reviewed intermediate results, rejected weak directions, and selected inputs for the next round.
• Agents assisted with tensor calculations, candidate construction, manuscript preparation, and internal proof checks.
• Humans chose the mathematical strategy, assessed validity, and assembled the final argument.

The team also ran repeated unguided attempts with several leading models, using approximately the same total token budget as the supervised process. Those attempts did not solve the problem. Within this project, iterative human selection made the available model output substantially more useful than end-to-end prompting.

Three proofs converge

A separate group of experts posted a full proof on the same day as the completed Microsoft paper. That group developed its work in parallel and credited a criterion from the first Microsoft draft as “the crucial step in the proof.” A third proof released that day used a closely related idea.

A public Lean 4 formalization combines the Microsoft criterion with additional work. Lean checks each encoded inference against a small logical kernel, providing a mechanical audit of the formalized argument. The Microsoft authors also report formalizing a shorter version of their proof, with publication planned after review.

Which guarantees change

The exact effect on any algorithm depends on where KLS enters its proof. Other dimension-dependent terms may still dominate the runtime, and distributions outside the log-concave setting receive no automatic benefit. Libraries and application code therefore gain no immediate speedup from the theorem alone.

Constants still need work

The proof establishes a universal constant without optimizing it for numerical use. Researchers can now remove a major asymptotic assumption, while sharper constants and implementation-level consequences remain separate problems. Practical improvements will require tracing the new bound through individual sampling and optimization analyses, then determining whether it changes parameter choices or measured performance.

A supervised research pattern

The project documents a concrete model for AI-assisted mathematics: agents generate and calculate across many branches, while researchers repeatedly evaluate those branches and set the next objective. The unguided control, independent proofs, and formal checks make the workflow unusually inspectable. Its evidence applies directly to this project and offers a process that other research teams can test on similarly calculation-heavy problems.