SorryDB: Can AI Provers Complete Real-World Lean Theorems?
Authors: Austin Letson, Leopoldo Sarra, Auguste Poiroux, Oliver Dressler, Paul Lezeau, Dhyan Aranha, Frederick Pu, Aaron Hill, Miguel Corredera Hidalgo, Julian Berman, George Tsoukalas, Lenny Taelman
Organizations: Axiomatic AI · Math, Inc. · EPFL · Imperial College · The London School of Geometry and Number Theory · University of Amsterdam · Côte d’Azur University · University of Toronto · ENSEIRB-MATMECA, INP-Bordeaux · Columbia University · The University of Texas at Austin
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.
Figures & tables
Figure 1: Dataset extraction pipeline for SorryDB. We consider 78 repositories of active GitHub Lean projects and list all the theorems that contain a sorry. We save the metadata for each of them and store it in the database. A project is considered active when it had at least one commit in the previous three months.
Category
SorryDB-2601
Test Sample
Formalization
3,099
562
Pedagogical
1,037
216
Benchmark
797
48
Library
616
89
Tooling
114
85
Total
5,663
1,000
Table 1: Distribution of sorry statements by repository category in the SorryDB-2601 dataset snapshot and for the specific 1000 sorry statements we sampled for use in our experiments. For building the latter, we sampled the newest sorry statements from each repository to maximize diversity and recency.
Figure 2: 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.
Approach
Pass@1
Pass@32
Deterministic
Trivial
2.1 %
n/a
Tactics
8.4 %
n/a
General-purpose LLM
GPT 5.2
6.2 %
13.2 %
Claude Opus 4.5
7.8 %
15.4 %
Table 2: Performance of various provers on a snapshot of 1000 tasks from SorryDB-2601 . Tactics are deterministic and thus only evaluated once. General-purpose and specialized models are evaluated by sampling once (pass@1) or by checking if any of 32 candidates solve the task (pass@32). Self-correcting (SC) or Agentic approaches run for up to 16 iterations. The row labelled as “Combined” shows how many tasks were solved by at least one prover. Since it is the largest value, it highlights the complementarity of the considered provers.
Figure 3: Number of solved tasks by number of LLM calls. Iterative sampling (self-correcting or agentic) is much more efficient than parallel sampling.
Figure 4: UpSet plot of sorry statements solved by each model. Each column represents the number of theorems solved by all the provers marked in the table with a black circle, and not solved by the others. Deterministic tactics solve some sorry statements that none of the LLM-based approaches could solve.
Appendix figures & tables11 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 6: Distribution of git blame dates in SorryDB-2601 and the 1000 sorry sample. Serving as a proxy for the time of addition, these dates reveal that most sorry statements are very recent.
Figure 7: Lean versions of SorryDB-2601 are distributed across major versions and release candidates with the vast majority of sorry statements on major versions 4.22, 4.24, 4.26, and 4.27.0-rc1, the last being the latest version at the time of the dataset collection.
Figure 8: Total sorry statements on GitHub over time have steadily increased over the last 3 years.
Figure 9: sorry statements added and removed from the Carleson project from its announcement to its completion. You can see sharp increases in number of sorry statements when new sections were added with missing proofs and then a gradual decrease as Lean practitioners provided proofs.
Table 4: Repositories in the SorryDB-2601 Dataset and number of sorry s per repository.
Figure 10: Number of sorry statements solved by each tactic. General purpose automation tactics like grind and aesop perform best.
Figure 11: UpSet plot of sorry statements solved by each tactic. Interestingly, exact? uniquely solves the most sorry statements, mostly from pedagogical repos. This makes sense as tutorials are likely to have exercises easily dispatched by theorems already in Mathlib. Grind is in second place, but solves sorry statements from a wider distribution of categories showing its versatility.
Figure 12: Token usage distributions for each model.
Strategy
Total Input
Total Output
Est. Cost
Tactics
0
0
N/A
gpt-5.2
112,360,153
8,339,934
$313.39
Claude Opus 4.5
135,067,959
17,036,984
$1,101.26
Gemini Flash 3
118,964,320
643,259,636
$1,989.26
Gemini Pro 3
114,786,853
448,730,558
$5,614.34
Kimina 8B
73,133,062
185,096,381
$482.10 *
Appendix
Table 5: Inference cost by strategy.
Figure 13: Distribution of sorry task difficulty in the SorryDB-2601 test sample, expressed as Elo ratings derived from head-to-head prover outcomes.
Name
Accuracy
Elo
Gemini Flash 3 (Agentic)
30.3%
1859
Gemini Flash 3 (SC)
27.9%
1775
Claude Opus 4.5 (SC)
27.1%
1751
Gemini Pro 3
20.6%
1582
Gemini Flash 3
20.5%
1579
Claude Opus 4.5
15.4%
1457
Appendix
Table 6: Elo ratings and accuracy of the evaluated provers on the SorryDB-2601 test sample.