Primary evidence
- SorryDB: Can AI Provers Complete Real-World Lean Theorems?S1 · Primary research · Paper · 2026-03-03
- SorryDB benchmark, verifier and proving infrastructureS1 · Primary research · Repository
SorryDB turns live proof holes from real Lean projects into a continuously updated benchmark
SorryDB crawls eligible public Lean repositories, records reproducible repository and toolchain coordinates for unresolved `sorry` statements, and asks proving systems to replace each proof hole in its original project context.
What happened?
The SorryDB paper introduced a dynamically updating benchmark of open Lean tasks drawn from 78 real-world formalization projects on GitHub, evaluated general-purpose models, specialized provers and agentic strategies on a 1,000-task snapshot, and released the dataset, verifier and strategy infrastructure publicly.
SorryDB crawls eligible public Lean repositories, records reproducible repository and toolchain coordinates for unresolved `sorry` statements, and asks proving systems to replace each proof hole in its original project context. A verifier rebuilds the relevant project and checks proposed replacements, while a nightly database refresh supplies new tasks over time.
Why it matters
A live benchmark grounded in unresolved work from real formalization projects reduces reliance on saturated competition datasets, exposes dependency and environment complexity that synthetic tasks omit, and aligns prover progress more directly with work useful to Lean contributors and mathematicians.
Significance rationale: SorryDB shifted formal-theorem-proving evaluation from mostly static curated theorem sets toward continuously refreshed, reproducible proof obligations taken from active public Lean projects, directly measuring whether AI agents can contribute to real formalization codebases.
Historical context
Earlier developments
Later developments
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E3 · Inspectable artifact
- AI role
- Computation only
- Formal assurance
- Artifact available
Contribution & verification
- Mathematical novelty
- Benchmark result
- Interface
- Formal
- AI contribution
- AI systems are benchmarked as candidate proof producers; they generate tactics or proofs, while the benchmark infrastructure restores the original project context and Lean checks whether a proposed replacement closes the target proof hole.
- Human contribution
- Researchers designed the crawling, snapshotting, evaluation and verification infrastructure, defined inclusion and reproducibility metadata, implemented baseline strategies and analyzed the benchmark results.
- Verification
- Paper released · E3 · Inspectable artifact · Artifact available
- Last reviewed
- 2026-09-11
Technical details
- Systems
- sorrydb, lean
- Organizations
- sorrydb
- Problems
- real-world-lean-proof-holes, formal-theorem-proving-evaluation
- Methods
- live-benchmarking, repository-crawling, project-context-verification, agentic-proof-search, lean
Sources & artifacts
- SorryDB: Can AI Provers Complete Real-World Lean Theorems?S1 · Primary research · Paper · accessed 2026-09-11
- SorryDB benchmark, verifier and proving infrastructureS1 · Primary research · Repository · accessed 2026-09-11
- SorryDB dynamic Lean benchmark and evaluation infrastructureArtifact · Benchmark
Verification history
- 2026-03-03 · Paper released · E2 · Research record
The arXiv paper introduced SorryDB, its 78-project source pool, the 1,000-task evaluation snapshot and comparative prover results.
- 2026-09-11 · Paper released · E3 · Inspectable artifact
The public SorryDB repository exposes the benchmark snapshot, nightly dataset workflow, verifier and example proving strategies. E3 records inspectable benchmark infrastructure rather than independent verification of every reported model score.
Corrections
No corrections recorded.