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

The paper introduces SorryDB, a dynamic benchmark of real-world Lean formalization tasks designed to better align AI provers with community needs and mitigate test contamination, revealing that current approaches including agentic models, general LLMs, and specialized provers are complementary rather than one strictly dominating the others.

The Gist

The "Sorry" Database: Teaching AI to Finish Real Math Homework

Imagine you are a brilliant but slightly overwhelmed math teacher. You have 78 different notebooks (GitHub repositories) filled with complex math problems. You've written down the questions and the setup for the proofs, but you haven't finished the answers yet. Instead of leaving them blank, you've stuck a little sticky note on the unfinished parts that says "Sorry, I'll do this later."

In the world of the computer language Lean (used for formal math), this sticky note is literally the word sorry.

This paper introduces SorryDB, a new way to test Artificial Intelligence. Instead of asking AI to solve old, well-known math puzzles (like Olympic math problems), the researchers built a database of these "Sorry" sticky notes from real, active math projects. They want to see if AI can actually help mathematicians finish their real-world work.

Here is the breakdown of the paper using simple analogies:

1. The Problem: The "Olympiad" Trap

For years, we tested AI math brains using Math Olympiads (like the Putnam competition).

• The Analogy: Imagine testing a race car driver only on a perfectly smooth, empty racetrack with no traffic.
• The Issue: Real math isn't a racetrack. It's like driving through a messy city with construction, traffic jams, and weird detours. Real math projects depend on thousands of other definitions and theorems written by other people.
• The Result: AI models got really good at the "racetrack" (Olympiads) but struggled when asked to fix a real, messy math project. Also, the AI might have just memorized the answers to the old Olympiad problems, so we didn't know if they were actually thinking.

2. The Solution: The "Sorry" Database

The researchers went to GitHub and found 78 active math projects. They looked for every single place where a human mathematician said, "I'm stuck, I'll finish this later" (the sorry keyword).

• The Analogy: Instead of giving the AI a fresh, clean test paper, they handed it a pile of half-finished homework assignments from real students.
• Why it's better:
  • Fresh: These problems haven't been solved yet, so the AI can't cheat by memorizing the answer.
  • Real: The problems are messy, depend on specific libraries, and require understanding the context of the whole project.
  • Moving Target: As soon as an AI solves a "Sorry," the database updates with new, harder ones. It's a benchmark that never gets "saturated" (stale).

3. The Experiment: Who Can Finish the Homework?

The researchers took a snapshot of 1,000 of these "Sorry" tasks and asked different types of AI to solve them. They tested three main types of "students":

• The "Tactics" (The Calculator): These are pre-programmed commands (like grind or linarith) that can solve simple, mechanical math problems instantly.
  • Result: Good for easy stuff, but can't handle complex reasoning.
• The "Generalists" (The Smart Librarian): These are huge AI models (like Gemini, Claude, GPT) that know a little bit about everything. They try to write the proof in one go.
  • Result: They are decent, but often get lost in the details or hallucinate (make up) facts.
• The "Agents" (The Detective): These are AI models that don't just guess; they have a workflow. They can look up information, try a solution, see if it fails, read the error message, and try again.
  • Result: The Winners. The "Agent" approach (specifically one based on Gemini Flash) was the best.

4. Key Discoveries (The "Aha!" Moments)

A. Feedback is the Secret Sauce
The most successful AI didn't just guess; it iterated.

• The Analogy: Imagine trying to fix a broken toaster.
  • One-shot AI: Guesses a fix, tries it, and if it fails, it gives up.
  • Agent AI: Guesses a fix, tries it, sees the smoke, reads the error ("Oh, the wire is too short"), and tries again with a longer wire.
• Finding: AI that could "read the error message" and try again (Self-Correcting) solved 30% of the problems, while AI that just guessed once only solved 10%.

B. No One is Perfect (Complementarity)
No single AI model solved everything.

• The Analogy: Think of a sports team. The "Tactics" are the goalkeepers (great at stopping simple shots). The "Generalists" are the strikers (good at big plays). The "Agents" are the midfielders (good at connecting the play).
• Finding: If you combine all the AI models, they solved 35% of the problems. If you only used the best single model, you'd miss out on the problems the others solved. They are all needed.

C. The "Tool" Trap
Some AI models tried to use a search tool to find the answer, but they got distracted.

• The Analogy: A student trying to do math who keeps opening Google instead of thinking.
• Finding: Sometimes, the AI that didn't use a search tool did better because it actually tried to construct the proof from scratch, rather than hoping to find a pre-made answer.

5. The Conclusion: Why This Matters

The paper argues that to build AI that actually helps mathematicians, we need to stop testing them on "fake" clean problems and start testing them on "real" messy work.

SorryDB is like a gym for AI mathematicians. It ensures that as AI gets smarter, the tests get harder, preventing the AI from just memorizing answers. It shows that the future of AI math isn't just about having a bigger brain; it's about having a better workflow—one that can read errors, search for help, and keep trying until the "Sorry" note is finally removed.

In short: We are moving from asking AI "Can you solve this riddle?" to asking "Can you help me finish this real project?" And the answer is getting closer to "Yes," especially if the AI is allowed to learn from its mistakes.

Technical Summary

1. Problem Statement

Current benchmarks for automated theorem proving (ATP) in Lean are increasingly saturated and misaligned with real-world applications.

• Limitations of Existing Benchmarks: Most datasets (e.g., miniF2F, PutnamBench) focus on competition math or undergraduate challenges. These tasks often lack the complex dependencies, local context, and "messiness" of large-scale formalization projects.
• Data Contamination: Because these benchmarks are static and public, solutions often leak into the training data of Large Language Models (LLMs), making it difficult to distinguish between genuine reasoning and memorization.
• The Gap: There is a lack of dynamic, real-world evaluation metrics that reflect the day-to-day work of mathematicians and formalizers, who often leave unproven theorems marked with sorry placeholders to be solved later.

2. Methodology: The SorryDB Framework

The authors introduce SorryDB, a dynamically updating benchmark derived from active open-source Lean projects on GitHub.

A. Dataset Construction

• Source: The dataset is extracted from 78 active repositories in the Lean Reservoir (the official Lean package registry).
• Selection Criteria: Repositories must be public, use an OSI-approved license, and have received at least one commit in the last three months (ensuring active development).
• Extraction Process:
  1. Identification: The system scans repositories for the sorry keyword, which acts as a placeholder for unproven theorems or intermediate steps.
  2. Filtering: Tasks are filtered to ensure they are reproducible, strictly require a proof (type Prop), and are deduplicated (keeping only the most recent occurrence).
  3. Categorization: Tasks are categorized into five groups: Pedagogical (tutorials), Tooling (Lean utilities), Benchmark (competition problems), Library (Mathlib), and Formalization (specific mathematical theories like Fermat's Last Theorem).
• Dynamic Nature: Unlike static datasets, SorryDB is designed to evolve. As AI tools solve existing sorry statements, new, harder ones naturally emerge in active projects, preventing saturation.

B. Evaluation Protocol

• Task Definition: The core task is "Fill-in-the-Sorry." The model must provide the code to replace a specific sorry keyword within a theorem context, not necessarily prove the entire theorem from scratch.
• Verification: A deterministic pipeline uses LeanInteract to verify solutions:
  1. The proposed code replaces the sorry.
  2. The project is compiled.
  3. The system checks that the specific proof obligation is discharged (no sorry remains at that location) and that the final state compiles without errors.
• Snapshot: The paper evaluates a static snapshot named SorryDB-2601 (cutoff Jan 2026), containing 5,663 total tasks, with a specific evaluation set of 1,000 tasks selected for recency and repository diversity.

3. Key Contributions

1. The SorryDB Dataset: A novel, dynamically evolving benchmark that aligns with practical formalization needs, mitigating data contamination and saturation issues.
2. Automated Validation Framework: A robust pipeline for verifying sorry-filling tasks by compiling real-world projects, ensuring that solutions are not just syntactically valid but mathematically correct within the project context.
3. Comprehensive Evaluation: A baseline assessment of diverse approaches (deterministic tactics, general LLMs, specialized provers, and agentic systems) on real-world tasks.

4. Experimental Results

The authors evaluated various models on the 1,000-task snapshot.

A. Performance Overview

• Iterative/Agentic Approaches Dominate: Models utilizing Self-Correction (SC) or Agentic loops (up to 16 iterations) significantly outperformed single-shot (pass@1) or parallel sampling (pass@32) approaches.
  • Gemini Flash 3 (Agentic): Achieved the highest success rate at 30.3%.
  • Gemini Flash 3 (SC): Achieved 27.9%.
  • Claude Opus 4.5 (SC): Achieved 27.1%.
  • In contrast, single-shot pass@32 for the best general LLM (Gemini Flash 3) was only 20.5%.
• Complementarity: No single model solved all tasks. The "Combined" success rate (any model solving a task) reached 35.7%, indicating that different provers excel at different subsets of problems.
• Deterministic Tactics: Simple tactics (e.g., trivial, ring, grind) solved 8.4% of tasks, proving that some real-world problems are solvable without heavy LLM reasoning.

B. Key Findings

• Context is King: Iterative approaches that receive build error feedback (compilation errors) perform much better than those with larger reasoning budgets but no feedback. Access to the project environment is critical.
• Domain Specificity:
  • Pedagogical/Benchmark tasks were easier to solve (often solvable by existing Mathlib lemmas).
  • Formalization tasks (e.g., Carleson's Theorem, FLT) were the hardest.
  • Specialized models (e.g., Goedel Prover V2) performed well on benchmark tasks but struggled on general formalization projects, likely due to training on older Lean versions or specific competition domains.
• Tool Reliance vs. Construction: A qualitative analysis revealed a counter-intuitive failure mode: an agentic model relying heavily on search tools (LeanSearch) sometimes failed to solve a problem because it kept searching for non-existent lemmas, whereas a self-correcting model without tools succeeded by manually constructing the proof term.

5. Significance and Future Directions

• Shift in Evaluation: SorryDB moves the field away from "olympiad-style" math problems toward the practical utility required for large-scale mathematical formalization.
• Moving Benchmark: By continuously updating, SorryDB ensures that as AI capabilities improve, the benchmark difficulty scales accordingly, preventing the "saturation" seen in static datasets.
• Practical Utility: The results suggest that for real-world theorem proving, iterative refinement with compiler feedback is more effective than pure reasoning or massive parameter counts alone.
• Limitations: The current verifier restricts solutions that require adding new imports or defining new lemmas outside the immediate scope, which may limit the expressivity of some provers. Future work aims to relax these constraints and implement Elo-style scoring.

In conclusion, SorryDB demonstrates that while current AI provers are not yet fully autonomous in solving complex real-world theorems, agentic approaches with iterative feedback are the most promising path forward, and the community needs dynamic benchmarks to drive genuine progress in automated formal reasoning.