LLM writes Lean proofs: 9 of 353 open Erdős problems solved, a few hundred dollars each

Instead of writing natural-language proofs, the model emits Lean proof code that the compiler checks step by step. Earlier work with this paradigm concentrated on competition mathematics and human-aided formalization of natural-language arguments, without a large-scale evaluation on open research-level problems. Run on all 353 Lean statements of Erdős problems then in the Formal Conjectures repository, it solved 9, and team experts confirmed each Lean statement faithfully captured the original conjecture.

The agent splits a proof into subgoals it can search independently, using compiler errors and an automated prover as feedback to fill in the proof sketch. The basic agent runs independent prover subagents with no shared state, while the full-featured agent coordinates them with an evolutionary algorithm and can call AlphaProof to close subgoals. The full-featured agent also proved 44 of 492 open OEIS conjectures and resolved an open question on Hilbert functions in algebraic geometry.

A post-hoc comparison on the 9 solved Erdős problems shows the simplest agent design also solved all of them, at higher cost on the hardest ones. When the large-scale exploration was planned, simpler agentic loops did not show strong performance on competition-level benchmarks, which drove the choice of the full-featured agent. On Erdős #138 and #125 the full-featured agent saved 2x to 5x in cost over the basic configurations, but was roughly half as cost-efficient on the remaining problems.

The agent targets open problems that already have Lean formalizations: it takes a proof sketch with a sorry placeholder and returns a sorry-free proof. It has been used in combinatorics, optimization, graph theory, algebraic geometry and quantum optics, with the quantum optics and graph theory efforts still ongoing. The authors propose characterizing and expanding the agents' boundaries as a direction for future work.

The authors note that successes are concentrated where Lean's mathematics library is mature and tasks often decompose into tractable subgoals; most Erdős problems remain out of reach, let alone problems requiring extensive new theory. The agents inherit the biases of their underlying LLMs and exhibit high search variance, per-problem costs vary widely, and the reported costs exclude the compute spent identifying tractable problems. The full-featured agent's advantage on the hardest problems may diminish as LLM capabilities grow.