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

Nikil Ravi; Kexing Ying; Vasilii Nesterov; Rayan Krishnan; Elif Uskuplu; Bingyu Xia; Janitha Aswedige; Langston Nashold

cs.AIMar 27, 2026

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

Authors: Nikil Ravi, Kexing Ying, Vasilii Nesterov, Rayan Krishnan, Elif Uskuplu, Bingyu Xia, Janitha Aswedige, Langston Nashold

Organizations: Vals AI · École Polytechnique Fédérale de Lausanne (EPFL) · Moscow Institute of Physics and Technology · Indiana University, Bloomington · Independent Researcher

Abstract

We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.

Figures & tables

Panel of Figure 1 — Figure 1: Evaluation pipeline for FormalProofBench. Models are given the informal problem statement, along with the formalized statement (+ necessary headers and context), and have 40 turns (with each turn potentially involving multiple tool calls and reasoning), to submit a proof.

Subject Area	Count
Real Analysis	56
Probability Theory / Stochastic Analysis	34
Functional Analysis	26
Number Theory	23
Logic / Model Theory	21
Algebra	18

Table 1: Breakdown of FormalProofBench problems by subject area.

Rank	Model	Acc. (%)	Cost / test ($)	Latency (s) / test
1	Claude Opus 4.5 (Thinking)	33.50	1.34	4036.78
2	Gemini 3 Pro (11/25)	18.50	1.26	9966.43
3	Claude Sonnet 4.5 (Thinking)	18.00	0.84	11186.79
4	GPT 5	17.00	0.89	5017.28
5	Gemini 3 Flash (12/25)	15.00	0.33	1305.37
6	GPT 5.2	13.50	1.10	1459.24

Table 2: FormalProofBench overall leaderboard results (accuracy (in %), cost per test, and latency per test).

Figure 4: Total tool calls (search vs. code execution) aggregated across all 200 problems per model. Models vary widely in their tool-use strategies.

Figure 5: We observe a positive but modest correlation between the number of code execution calls and accuracy across models. Notable outliers include GPT 5, which achieves relatively high accuracy with very few code execution calls, and Grok 4.1 Fast, which executes substantial code but achieves low accuracy.

Explore similar work

Pseudo-Formalization for Automatic Proof Verification
May 19, 2026Slim Barkallah, Luke Bailey, Kaiyue Wen +2Mathematical Reasoning Benchmarks LLM-as-a-Judge
Stanford University
LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
Jun 2, 2026Po-Nien Kung, Linfeng Song, Dawsen Hwang +10Mathematical Reasoning Benchmarks Automated Theorem Proving
Google Cloud AI Research · Google Cloud · Google DeepMind
MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize
Aug 26, 2026Jiaxin Yuan, Connor Martinez Lockhart, Xiaoyu Liu +11Mathematical Reasoning Benchmarks Automated Theorem Proving
University of Maryland, College Park · Georgia Institute of Technology · Cornell University +2

May 19, 2026J/K move · Enter open · S save

Pseudo-Formalization for Automatic Proof Verification

Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid+1

Stanford University

Mathematical Reasoning Benchmarks LLM-as-a-Judge Autoformalization

Open paper AskPDF arXiv

Reliable verification of proofs remains a bottleneck for training and evaluating AI systems on hard mathematical reasoning. Fully formal proofs, in languages like Lean, are easy to verify because they are unambiguous and modular. Most proofs, particularly those written by AI systems, have neither property, and translating them into formal languages remains challenging in many frontier math settings. We propose Pseudo-Formalization (PF), a proof format that captures the modularity and precision of formal proofs while retaining the flexibility of natural language. A Pseudo-Formal proof is decomposed into self-contained modules, each stating its premises, conclusion, and proof in natural language. To verify the correctness of a regular natural language proof, an LLM translates it to Pseudo-Formal and then verifies each module independently, an algorithm we call Block Verification (BV). We evaluate PF+BV on two benchmarks spanning olympiad and research-level mathematics, where it pareto-dominates LLM-as-judge baselines on error-finding precision and recall. To support future work, we release our research-level proof verification benchmark ArxivMathGradingBench.

Abstract

Explore similar work

Pseudo-Formalization for Automatic Proof Verification

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize