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.
@article{arxiv.2603.26996,
title = {FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?},
author = {Nikil Ravi and Kexing Ying and Vasilii Nesterov and Rayan Krishnan and Elif Uskuplu and Bingyu Xia and Janitha Aswedige and Langston Nashold},
journal= {arXiv preprint arXiv:2603.26996},
year = {2026}
}
Comments
Accepted at ICLR 2026 Workshop: VerifAI-2: The Second Workshop on AI Verification in the Wild. Live leaderboard hosted here: https://www.vals.ai/benchmarks/proof_bench