On October 21, Microsoft Research said Xinzhi Zhang and Zhao Song had proved the Kannan–Lovász–Simonovits conjecture, a math problem posed in 1995. In the Microsoft Research announcement, the company says the result came from a human-directed agent workflow rather than a fully autonomous model run.
Microsoft says AI systems explored more than 100 candidate approaches, while the researchers chose which branches to pursue, cut weak paths, and checked the surviving mathematics. The company also says unguided attempts with several leading models and roughly the same total token budget did not solve the problem.
The post says the tools were used beyond idea generation, including derivations, drafting the paper, and internal proof checks. Microsoft adds that a Lean 4 formalization has already been released, with a shorter machine-verified version planned after final review.
It is still best read as an important preprint result, not a settled textbook milestone. Independent reports said other groups posted parallel proofs within days, which adds confidence, but the work has not yet gone through journal review.