A new agentic system can take a research-level math paper and produce a formally verified proof — one a computer can check line by line.
Researchers built a multi-agent pipeline around general-purpose coding LLMs, which recent benchmarks show now outperform models specifically fine-tuned for the Lean 4 proof language. The system's core trick is handling math that doesn't exist yet in standard libraries like Mathlib: an orchestrator dynamically defines new types and validates them using what the authors call an Auxiliary Lemma technique before attempting to formalize the main theorems. The team tested it on 32 problems from PutnamBench and on five papers from the ACM Symposium on Theory of Computing, spanning combinatorics, communication complexity, mechanism design, and learning theory. Human experts validated the results, and two of the five papers yielded proofs requiring no axioms beyond Lean's built-in kernel.
LLMs are notoriously good at math that looks right but isn't — subtle errors that slip past human reviewers. Plugging those outputs into a formal proof checker closes that loop in a way that peer review alone cannot. If the approach scales, it could shift the bar for what counts as a verified result in theoretical computer science.
The obvious caveat: five papers is a small sample, the problems were chosen by the researchers, and "successfully formalizing" still required human expert sign-off at the end. Impressive proof of concept — emphasis on concept.