# SorryDB: Can AI Provers Complete Real-World Lean Theorems?

arXiv: https://arxiv.org/abs/2603.02668 · HTML: https://mlsanity.com/paper/2603.02668/

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- Builds on 35 of its 57 references that are in the map.
- First posted on arXiv 3 Mar 2026.

## Builds on (most cited first, 30 of 35)

- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Gemini 2.5: Pushing the Frontier with Advanced Reasoning, Multimodality, Long Context, and Next Generation Agentic Capabilities](https://mlsanity.com/paper/2507.06261/) (2025)
- [SWE-bench: Can Language Models Resolve Real-World GitHub Issues?](https://mlsanity.com/paper/2310.06770/) (2023)
- [Mastering Chess and Shogi by Self-Play with a General Reinforcement Learning Algorithm](https://mlsanity.com/paper/1712.01815/) (2017)
- [CodeSearchNet Challenge: Evaluating the State of Semantic Code Search](https://mlsanity.com/paper/1909.09436/) (2019)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition](https://mlsanity.com/paper/2504.21801/) (2025)
- [SWE-bench Multimodal: Do AI Systems Generalize to Visual Software Domains?](https://mlsanity.com/paper/2410.03859/) (2024)
- [Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning](https://mlsanity.com/paper/2504.11354/) (2025)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correction](https://mlsanity.com/paper/2508.03613/) (2025)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [BetterBench: Assessing AI Benchmarks, Uncovering Issues, and Establishing Best Practices](https://mlsanity.com/paper/2411.12990/) (2024)
- [Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving](https://mlsanity.com/paper/2507.23726/) (2025)
- [Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline](https://mlsanity.com/paper/2507.15855/) (2025)
- [Hilbert: Recursively Building Formal Proofs with Informal Reasoning](https://mlsanity.com/paper/2509.22819/) (2025)
- [miniCTX: Neural Theorem Proving with (Long-)Contexts](https://mlsanity.com/paper/2408.03350/) (2024)
- [LeanAgent: Lifelong Learning for Formal Theorem Proving](https://mlsanity.com/paper/2410.06209/) (2024)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [VERINA: Benchmarking Verifiable Code Generation](https://mlsanity.com/paper/2505.23135/) (2025)
- [A Semantic Search Engine for Mathlib4](https://mlsanity.com/paper/2403.13310/) (2024)
- [SWE-Bench++: A Framework for the Scalable Generation of Software Engineering Benchmarks from Open-Source Repositories](https://mlsanity.com/paper/2512.17419/) (2025)
- [FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levels](https://mlsanity.com/paper/2511.02872/) (2025)
- [MA-LoT: Model-Collaboration Lean-based Long Chain-of-Thought Reasoning enhances Formal Theorem Proving](https://mlsanity.com/paper/2503.03205/) (2025)
- [A Minimal Agent for Automated Theorem Proving](https://mlsanity.com/paper/2602.24273/) (2026)
- [Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Models](https://mlsanity.com/paper/2506.11487/) (2025)
- [CodeClash: Benchmarking Goal-Oriented Software Engineering](https://mlsanity.com/paper/2511.00839/) (2025)
- [RLMEval: Evaluating Research-Level Neural Theorem Proving](https://mlsanity.com/paper/2510.25427/) (2025)

## Built on by (most cited first, 8 of 8)

- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?](https://mlsanity.com/paper/2603.26996/) (2026)
- [Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness](https://mlsanity.com/paper/2605.10379/) (2026)
- [s2n-bignum-bench: A practical benchmark for evaluating low-level code reasoning of LLMs](https://mlsanity.com/paper/2603.14628/) (2026)
- [AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics](https://mlsanity.com/paper/2609.05157/) (2026)
- [SqueezeBench: Saturation-Resilient Evaluation of Mathematical Capability](https://mlsanity.com/paper/2610.13461/) (2026)
- [The Future of AI-assisted Physics: Discovering, Verifying and Organizing Results via Formalization](https://mlsanity.com/paper/2610.14059/) (2026)
- [A dataset of formalised theorem statements from the Annals of Mathematics](https://mlsanity.com/paper/2610.18301/) (2026)

## Abstract (arXiv)

We present SorryDB, a dynamically-updating benchmark of open Lean tasks drawn from 78 real world formalization projects on GitHub. Unlike existing static benchmarks, often composed of competition problems, hillclimbing the SorryDB benchmark will yield tools that are aligned to the community needs, more usable by mathematicians, and more capable of understanding complex dependencies. Moreover, by providing a continuously updated stream of tasks, SorryDB mitigates test-set contamination and offers a robust metric for an agent's ability to contribute to novel formal mathematics projects. We evaluate a collection of approaches, including generalist large language models, agentic approaches, and specialized symbolic provers, over a selected snapshot of 1000 tasks from SorryDB. We show that current approaches are complementary: even though an agentic approach based on Gemini Flash is the most performant, it is not strictly better than other off-the-shelf large-language models, specialized provers, or even a curated list of Lean tactics.