A new benchmark shows that no AI system reliably fills in the unfinished proofs that real mathematicians leave behind.
Researchers built SorryDB by mining open "sorry" placeholders from 78 Lean formalization projects on GitHub, gaps where a human marked a theorem proof as incomplete and moved on. The dataset refreshes continuously, which sidesteps the contamination problem that plagues static benchmarks: once AI labs know a fixed test set, training pipelines can inadvertently absorb those examples. The team evaluated a snapshot of 1,000 tasks against a range of systems, including generalist large language models, agentic frameworks, and specialized symbolic provers. A Gemini Flash-based agentic approach scored highest overall, but no single method was strictly better than all the others; each tool class found proofs the rest missed.
That complementary result is the more interesting finding. It suggests that the gap between "AI can solve olympiad problems" and "AI can assist working mathematicians" will not close by scaling one type of system. Real formalization projects carry tangled cross-file dependencies and evolving context that competition problems, with their clean self-contained structure, do not replicate.
The benchmark's name comes from Lean's own syntax: a sorry is a placeholder that compiles but proves nothing, which is a serviceable summary of where AI theorem proving still stands.