SorryDB: Evaluating the real-world capabilities of automated verification tools

Summary

While AI models can generate impressive solutions, they remain highly prone to hallucinations. Formal verification through proof assistants like Lean offers a fix, acting as the ultimate ground-truth checker. However, we currently test these AI provers on static, narrowly defined benchmarks, primarily based on competition math.

SorryDB changes this. Hosted in its own independent GitHub organization, SorryDB is a community-owned dataset and benchmark built by and for Lean practitioners. While Axiomatic AI employs some of the project’s core contributors, it is fundamentally collaborative. By evaluating provers in these real-world settings, the community ensures that high performance on a benchmark actually translates into practical, real-world usefulness.

How does it work?

SorryDB indexes Lean packages and formalization projects from the Reservoir package index, the equivalent of PyPI for Lean. In Lean, developers use the sorry keyword as a literal placeholder for a missing proof, essentially telling the compiler, “I will prove this later.” SorryDB collects these sorry statements, extracts the underlying proof holes, and filters them. Then these tasks are assembled into a standardized, dynamically evolving benchmark that continuously reflects the frontier of community needs. For information about how Lean packages are selected for SorryDB, see the section in the README for project maintainers.

Figure: SorryDB is a dynamically updating benchmark of open Lean tasks drawn from real-world formalization projects on GitHub.

Why sorry statements reflect real project work

In many large formalization projects, contributors first establish definitions, interfaces, and theorem statements, leaving selected proofs as sorry statements for later work. New development therefore creates visible spikes in unresolved obligations, followed by gradual declines as contributors complete them.

The Carleson project illustrates this pattern. Major additions introduced batches of new sorry declarations, which were subsequently removed as the formalization progressed. SorryDB uses these naturally occurring proof obligations as a testbed for systems intended to assist with the same work.

Figure: Sorry statements added and removed from the Carleson project from its announcement to its completion. When new sections are added with missing proofs, there are sharp increases in the number of sorry statements and then a gradual decrease as Lean practitioners provide proofs.

Evaluation results

To see how modern provers handle the messy reality of open-source mathematics, we evaluated a spectrum of models against a 1,000-task sample of SorryDB-2601. This slice was explicitly selected to capture the newest sorry statements while maximizing the diversity of the underlying repositories.

We tested four main approaches: baseline deterministic tactics (ranging from trivial commands to SMT-based engines like grind), general foundation models (Claude Opus 4.5, Gemini Flash 3, GPT 5.2, Qwen 3), specialized theorem provers (Kimina-prover, Goedel-Prover V2), and self-correcting agentic loops. The strongest agentic configuration solved 30.3% of tasks overall, compared with 20.5% for the best single-shot foundation model and 11.3% for the best specialized prover.

The evaluations revealed three major themes about the current state of automated theorem proving:

• Formalization projects are harder than pedagogical and benchmark repos. Across all methods, tasks pulled from pedagogical repositories (like university course materials) were consistently easier to solve.
• Specialized provers show a generalization gap. Models like Goedel Prover performed relatively well on tasks drawn from benchmark repositories. However, when asked to clear a sorry in a standard library or novel formalization project, their performance degraded.
• Agency and iteration beat single-shot prediction. Wrapping a foundation model like Gemini Flash 3 in an agentic ReAct loop, where it can search Lean libraries and use up to 16 attempts to fix its own compilation errors, proved most effective.

Figure: Success rate of different provers split by repository category. We compare general purpose LLMs, specialized models (pass@32), self-correcting (SC) and agentic approaches (16 iterations). We see that tasks from pedagogical repositories are easier to prove, while those from math formalization projects are harder. A specialized prover such as Goedel Prover works relatively better on benchmark repositories but has worse performance on other project types.

Scaling SorryDB with MorphCloud

Evaluating provers on real-world Lean repositories introduces an engineering challenge. Unlike static, isolated benchmark problems, the repos we use are living software projects. Each one relies on different Lean versions, package dependencies, and custom Lake configurations. Setting up these environments dynamically for each test case is computationally unfeasible.

To scale SorryDB evaluations and avoid rebuilding complex Lean toolchains on every run, we partnered with MorphCloud to handle the heavy lifting. We spin up a VM instance, ingest the target project, compile and cache the exact environment needed for that specific sorry task, and capture the final build as a snapshot.

This MorphCloud instance snapshot approach unlocks two major capabilities for SorryDB:

1. Parallelization: With the environment perfectly frozen, we can clone the snapshot and evaluate dozens of different provers or agentic loops simultaneously without redundant build times.
2. Reproducibility: If a new open-source prover or an updated version of AxProverBase is released next month, we can spin up the exact same cached “sorry snapshot.”

A Continuously Evolving Challenge

As the capabilities of automated provers improve, the difficulty of proof holes posted on GitHub in formalization projects naturally scales. If a hole can be automatically closed with existing tools, it is likely that it will be closed. Because new releases track newly introduced proof holes, SorryDB is designed to resist benchmark saturation and evolve alongside the needs of the Lean community.

We recently presented this work at ICML.

• Check the leaderboard: See how the latest state-of-the-art models stack up against the current benchmark by visiting the SorryDB Leaderboard.
• Read the paper: To dive deeper into the methodology, environment caching, and full evaluation results, read the full paper on arXiv.
• Test your models: If you are building automated provers and want to test them against the frontier of formal mathematics, check out the SorryDB dataset and benchmark on GitHub.