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

• URL: http://arxiv.org/abs/2603.26996v1
• Date: Fri, 27 Mar 2026 21:14:53 GMT
• Title: FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
• Abstract summary: We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs.<n>Each task pairs a natural-language problem with a Lean4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker.<n>We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy.
• Score: 0.04324039930655099
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• MathAdv: What Theorem Provers Know, Reason, Formalize, and Generalize [38.37332307303914]
  MathAdv is a diagnostic benchmark spanning 13 domains across undergraduate- and graduate-level mathematics.<n>We show how component-wise evaluation can reveal model capabilities and failure modes that aggregate theorem-proving accuracy obscures.
  arXiv  Detail & Related papers  (2026-08-26T07:12:54Z)
• MathCoPilot: An Interactive System for Human-AI Symbiotic Paradigm of Mathematical Research [62.221184989046826]
  MathCoPilot is a human-in-the-loop system that embodies a new human--AI symbiotic paradigm for mathematical research.<n>MathCoPilot unifies three core capabilities: an interactive proof blueprint that decomposes a proof into navigable steps the human can directly inspect, direct, and refine; automated proving skill orchestration with adaptive knowledge base search and Lean-integrated iterative verification; and topic-driven paper retrieval and automated formalization into a verified Lean knowledge base.
  arXiv  Detail & Related papers  (2026-07-16T05:22:40Z)
• AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification [41.90353470982016]
  Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics.<n>Existing benchmarks fall short in both scope and evaluation granularity.<n>We introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities.
  arXiv  Detail & Related papers  (2026-07-13T17:38:22Z)
• LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks [85.86474267842907]
  Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate verifiable proofs in formal languages like Lean.<n>We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving.
  arXiv  Detail & Related papers  (2026-06-02T08:16:42Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models [11.250861762443801]
  We introduce the RFMDataset (Reveal Failure Modes), a collection of 200 diverse mathematical proof problems.<n>We thoroughly evaluate advanced models' performance on it.<n>Our analysis uncovers 10 fine-grained error types, which shows fundamental limitations in current large reasoning models.
  arXiv  Detail & Related papers  (2025-06-20T16:14:18Z)
• Enumerate-Conjecture-Prove: Formally Solving Answer-Construction Problems in Math Competitions [39.102692814217086]
  LLMs can tackle difficult answer-construction tasks but are prone to errors from hallucinations and unverifiable steps.<n>This raises a key understudied question: how to solve answer-construction problems while preserving both creativity and mathematical rigor?<n>We introduce the LLM-Conjecture-Prove (ECP) framework, a neuro-symbolic method integrating pattern-driven conjecturing with formal theorem proving.<n>On ConstructiveBench, ECP achieves 33.1% end-to-end state-of-the-art accuracy (up from 32.5%), demonstrating its potential to advance formal mathematical reasoning.
  arXiv  Detail & Related papers  (2025-05-24T03:52:25Z)
• Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchically [29.908878832382523]
  This paper focuses on improving LLMs' ability to write proofs in formal languages that permit automated proof verification/evaluation. We work in a more natural setup where the lemmas that are directly relevant to the theorem are not given to the theorem prover at test time. We design an RL-based training algorithm that encourages the model to decompose a theorem into lemmas, prove the lemmas, and then prove the theorem by using the lemmas.
  arXiv  Detail & Related papers  (2024-11-04T05:57:40Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data [65.5290035371111]
  We introduce an approach to generate extensive Lean 4 proof data derived from high-school and undergraduate-level mathematical competition problems. We fine-tune the DeepSeekMath 7B model on this synthetic dataset, which comprises 8 million formal statements with proofs. Our model successfully proved 5 out of 148 problems in the Lean 4 Formalized International Mathematical Olympiad (FIMO) benchmark, while GPT-4 failed to prove any.
  arXiv  Detail & Related papers  (2024-05-23T09:03:42Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.