FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

The paper introduces FormalProofBench, a private benchmark for evaluating AI models' ability to generate formally verified graduate-level mathematical proofs in Lean 4, revealing that the best-performing model achieves only 33.5% accuracy while providing a comprehensive analysis of tool usage, failure modes, and efficiency.

The Gist

Imagine you are a teacher giving a math test to a class of very smart, but sometimes overconfident, robots.

In the past, these robots (AI models) were tested on math problems where they just had to write a solution in plain English. It was like asking them to write an essay on how to solve a puzzle. They could sound very convincing, using big words and logical-sounding sentences. But, just like a student who memorized the vibe of a proof without actually doing the math, they could hide tiny, fatal errors in their essays. A human teacher might miss a small mistake, and the robot would get a passing grade even though the answer was wrong.

The New Test: "FormalProofBench"

The authors of this paper created a new, much stricter test called FormalProofBench. Instead of writing an essay, the robots now have to write code in a very strict, unforgiving language called Lean 4.

Think of Lean 4 as a super-strict robot referee that never sleeps and never makes mistakes.

• If the robot's proof has even one tiny logical gap, a missing step, or a wrong definition, the referee immediately yells, "FAIL!" and stops the game.
• There is no "maybe," no "it sounds good," and no "I think this is right." It's binary: Pass or Fail.

The Setup: A 40-Turn Puzzle

The test isn't just a one-shot question. It's more like a video game level where the robot gets 40 turns to solve a graduate-level math problem.

• The Tools: The robot has a toolbox. It can look up rules in a giant digital library (Mathlib), run little test codes to see if a step works, and then finally submit its answer.
• The Goal: The robot has to take a complex math problem (like proving a theorem about probability or algebra) and translate it into Lean code that the referee accepts.

The Results: The Robots Are Getting Better, But Still Stumble

The researchers tested the world's smartest AI models (like Claude, GPT-5, and Gemini) on 200 of these hard problems. Here is what they found:

1. The "Thinking" Models Win: The best robot, Claude Opus 4.5, managed to solve about 33.5% of the problems. That might sound low, but remember: these are graduate-level math problems that even human PhD students struggle with.
2. The Drop-Off: After the top model, the scores dropped sharply. The next best models only solved about 18% or less.
3. The Secret Sauce (Tool Use): The paper discovered a fascinating pattern. The robots that did the best weren't just "thinking" hard; they were iterating.
   • Bad Strategy: Some robots kept asking the library for help (searching) over and over, getting stuck in a loop, like a person looking for a key in every drawer without ever trying the door.
   • Good Strategy: The winners used the "Run Code" tool constantly. They tried a step, saw it fail, fixed it, tried again, and saw it fail again. They treated the proof like a debugging session. The more they "ran the code" and got feedback, the better they did.

Why Does This Matter?

Think of this as a bridge between human intuition and machine certainty.

• Right now, AI is great at sounding smart (the "essay" phase).
• This test shows that AI is starting to learn how to be rigorous.

If AI can eventually pass this test with high scores, it means we won't just have robots that talk about math; we will have robots that can prove new mathematical truths without making mistakes. This could help human mathematicians verify their own work, discover new theorems, and ensure that the foundations of science are rock solid.

In a Nutshell:
The paper says, "We built a strict, automated math referee. The best AI robots are starting to pass the test, but they still make mistakes. The ones who succeed are the ones who aren't afraid to try, fail, fix, and try again, rather than just guessing."

Technical Summary

1. Problem Statement

While Large Language Models (LLMs) have shown significant progress in natural language mathematical reasoning (e.g., on MATH or GSM8K benchmarks), they often produce "plausible-sounding" arguments that contain subtle logical errors, omitted cases, or non-existent lemmas. These errors are difficult for human or automated graders to detect in natural language.

The core problem addressed is the lack of a rigorous, automated evaluation method for formal theorem proving at the graduate level. Existing benchmarks often focus on high-school competitions (Olympiads) or rely on informal grading. There is a need to determine if frontier AI models can generate machine-checkable proofs for advanced mathematics (undergraduate/graduate level) using Interactive Theorem Provers (ITPs) like Lean 4.

2. Methodology

2.1 Benchmark Construction (FormalProofBench)

• Scope: The benchmark consists of 200 problems drawn from advanced undergraduate and graduate sources, including qualifying exams and standard textbooks.
• Domains: Coverage includes Real Analysis, Probability/Stochastic Analysis, Functional Analysis, Number Theory, Logic/Model Theory, Algebra, Algebraic Geometry, and Linear Algebra.
• Format: Each task pairs a natural language problem statement with a corresponding Lean 4 formal statement.
• Quality Assurance: Problems were formalized by six PhD students/experts with significant Mathlib experience. A secondary human review process (GitHub code review) was implemented to prevent misformalization (where the formal statement does not match the informal intent).
• Contamination Resistance: The benchmark is kept private to prevent data contamination. Problems were selected to require knowledge beyond standard training data cutoffs and rely on specific, recent Mathlib additions.

2.2 Evaluation Harness (Agentic Loop)

Unlike single-pass generation, the evaluation uses an agentic harness allowing models to iterate:

• Input: Models receive the informal problem, the formal Lean 4 statement, necessary headers, and context.
• Tools:
  • lean_loogle: Searches for theorems/definitions in Mathlib.
  • lean_run_code: Executes Lean code to provide immediate feedback (errors, unsolved goals, type mismatches).
  • submit_proof: Final submission mechanism.
• Constraints: Models are allowed up to 40 turns per problem. A solution is valid only if it compiles successfully in the Lean 4 kernel (v4.25.2) without using axioms or sorry.
• System Prompt: Models are instructed to act as Lean 4 experts, adhering to specific syntax rules (e.g., CamelCase for lemmas, chaining tactics with ;).

3. Key Contributions

1. New Benchmark: Introduction of FormalProofBench, a deterministic, uncontaminated benchmark for graduate-level formal theorem proving.
2. Agentic Evaluation: Evaluation of frontier models using a multi-turn agent loop with access to search and code execution tools, rather than single-shot generation.
3. Comprehensive Analysis: Detailed reporting on accuracy, cost, latency, and tool-use patterns (search vs. execution).
4. Empirical Findings: Identification of specific failure modes and the correlation between tool usage strategies and success rates.

4. Results

4.1 Performance Overview

The evaluation covered 13 frontier models (OpenAI, Anthropic, xAI, Zhipu, Google, DeepSeek).

• Top Performer: Anthropic's Claude Opus 4.5 (Thinking) achieved the highest accuracy of 33.5%.
• Performance Drop-off: There is a sharp decline in performance after the top model. The second-best model (Gemini 3 Pro) achieved 18.5%, and the third (Claude Sonnet 4.5) achieved 18.0%.
• Bottom Performers: Several models scored below 5% (e.g., Grok 4.1 Fast at 4.0%, DeepSeek V3.2 Thinking at 3.0%).

4.2 Tool-Use Analysis

• Code Execution vs. Search: The study found a positive correlation between code execution frequency and accuracy.
  • Successful Strategy: Stronger models execute code early to get feedback, iterating on errors, and use the search tool (lean_loogle) only to fill specific gaps.
  • Failure Mode: Weaker models often "spiral" into excessive search calls, attempting to find non-existent lemmas without testing hypotheses via code execution.
• Latency & Cost: The average latency per test was high (often >1 hour due to the 40-turn limit and tool calls), with costs ranging from ~$0.10 to >$1.30 per problem.

5. Significance and Implications

• Verification over Plausibility: The benchmark proves that formal verification is a necessary step to distinguish between "plausible" reasoning and mathematically correct proofs. A proof either type-checks or it does not, eliminating the ambiguity of natural language grading.
• State of AI in Math: While 33.5% accuracy is a milestone, the rapid drop-off suggests that current models are not yet reliable autonomous agents for graduate-level mathematics. They struggle with complex type-class resolution and long-horizon planning in formal systems.
• Future of Mathematical Practice: As models improve, formal verification could transition from a niche expert skill to a standard tool for working mathematicians, enabling rapid exploration of proof strategies with immediate correctness feedback.
• Benchmarking Evolution: FormalProofBench addresses the "contamination" issue common in AI benchmarks by using private, freshly formalized problems, ensuring that scores reflect genuine reasoning capabilities rather than memorization.

Conclusion

FormalProofBench establishes a rigorous standard for evaluating AI in formal mathematics. It reveals that while frontier models are beginning to solve graduate-level formal proofs, significant gaps remain in their ability to navigate complex formal systems without human-like iteration and error correction. The paper highlights that iterative code execution is a critical success factor, suggesting that future improvements in theorem proving will depend heavily on agentic workflows rather than static generation.