LLMs increasingly excel at mathematical reasoning, but their unreliability limits research utility; generating formal proofs in languages like Lean mitigates this.
In the first large-scale evaluation on open problems, the most capable agent autonomously resolved 9 of 353 open Erdős problems and proved 44/492 OEIS conjectures.
The agent is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research; a basic generate-and-verify agent replicated the Erdős successes but proved costlier on the hardest problems.