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

arXiv: https://arxiv.org/abs/2603.26996 · HTML: https://mlsanity.com/paper/2603.26996/

## Key facts

- Cited by 5 papers in the map (data through 14 Oct 2026).
- Builds on 9 of its 21 references that are in the map.
- First posted on arXiv 27 Mar 2026.

## Builds on (most cited first, 9 of 9)

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?](https://mlsanity.com/paper/2506.06034/) (2025)
- [Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving on Inequalities](https://mlsanity.com/paper/2505.12680/) (2025)
- [SorryDB: Can AI Provers Complete Real-World Lean Theorems?](https://mlsanity.com/paper/2603.02668/) (2026)

## Built on by (most cited first, 5 of 5)

- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks](https://mlsanity.com/paper/2606.03303/) (2026)
- [Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness](https://mlsanity.com/paper/2605.10379/) (2026)
- [CAM-Bench: A Benchmark for Computational and Applied Mathematics in Lean](https://mlsanity.com/paper/2605.17255/) (2026)
- [StochBench: A Domain-Specific Benchmark for Stochastic Processes in Lean](https://mlsanity.com/paper/2609.09264/) (2026)

## Abstract (arXiv)

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.