Skip to content

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

🕒 Published (v1): 2026-03-27 21:14 UTC · Source: Arxiv · Venue: ICLR 2026 · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

FormalProofBench is a private, 200-problem benchmark of graduate-level mathematics requiring models to produce Lean 4 proofs accepted by the Lean kernel, evaluated through a multi-turn agentic harness with Mathlib search and code execution tools. The best frontier model (Claude Opus 4.5 Thinking) achieves only 33.5% accuracy, with a steep performance cliff below it. The binary, compiler-verified correctness signal eliminates the need for human or model grading.

Problem

Informal math benchmarks allow models to produce plausible but subtly flawed proofs that evade detection by human and LLM-based graders. Existing formal benchmarks (MiniF2F, PutnamBench, ProofNet) target competition or undergraduate difficulty, and typically evaluate single-shot proof generation rather than the iterative, tool-augmented workflow that real formalization requires.

Method

Each benchmark task pairs a natural-language problem statement with a Lean 4 formal statement. Models operate within an agentic harness providing three tools: lean_loogle (Mathlib semantic search via loogle.lean-lang.org), lean_run_code (execute Lean code and receive compiler feedback including error messages, unsolved goals, and type mismatches), and submit_proof (final submission). Models are given up to 40 turns per problem; a solution is valid iff the submitted proof compiles under Lean v4.25.2 with Mathlib (commit c98ae54). Proofs containing axiom or local_instance are rejected. The 200 problems span measure theory, real/functional analysis, algebra, algebraic geometry, number theory, probability/stochastic analysis, and logic, formalized by PhD students and domain experts with secondary GitHub-based review.

Key Contributions

  • A private, contamination-resistant benchmark of 200 graduate-level formal theorem proving tasks in Lean 4, drawn from qualifying exams and textbooks.
  • Deterministic binary evaluation via the Lean 4 kernel, removing the need for model-graded scoring.
  • A multi-turn agentic evaluation harness (up to 40 turns) with Mathlib search and code execution tools, matching realistic formalization workflows.
  • Comprehensive analysis of tool-use patterns, cost (per-problem averages ranging from ~\(0.05 to ~\)1.34), and latency (per-problem averages often exceeding one hour).
  • Finding that code execution frequency positively correlates with accuracy, while excessive search without execution correlates with failure.

Results

  • Claude Opus 4.5 (Thinking): 33.5% accuracy, $1.34/test, 4037 s/test
  • Gemini 3 Pro: 18.5%, $1.26/test, 9966 s/test
  • Claude Sonnet 4.5 (Thinking): 18.0%, $0.84/test, 11187 s/test
  • GPT 5: 17.0%, $0.89/test, 5017 s/test
  • Gemini 3 Flash: 15.0%, $0.33/test, 1305 s/test
  • GPT 5.2: 13.5%; GPT 5 Nano: 12.5%; GPT 5.1 Codex Max: 12.0%
  • DeepSeek V3.2 (Nonthinking): 8.0%; GPT 5 Mini: 7.0%; GLM 4.7: 4.5%; Grok 4.1 Fast: 4.0%; DeepSeek V3.2 (Thinking): 3.0%
  • GPT 5 is a notable outlier: high accuracy (rank 4) with very few code execution calls; Grok 4.1 Fast executes substantial code but achieves only 4.0%.

Limitations

  • Only 200 problems; limited statistical power for domain-specific breakdowns.
  • Benchmark coverage is constrained by what is currently formalizable in Mathlib, excluding cutting-edge research-level theorems.
  • The lean_loogle search tool proved significantly less useful than code execution; the interface may itself be a bottleneck rather than deeper model reasoning limits.
  • No ablation provided on the effect of omitting the natural-language statement (informal vs. formal-only input).
  • Private benchmark structure limits community reproducibility (sample problems and harness code are released, but not the full test set).
  • Evaluation at default provider sampling settings may not reflect optimized inference configurations.

Relevance to Harnesses / Meta-Harnesses

FormalProofBench is a direct instance of a domain-specific agentic harness: the evaluation framework itself is the contribution, wrapping a Lean kernel verifier, two tool interfaces (search and execution), and a 40-turn ReAct-style loop into a reusable scaffold for benchmarking formal reasoning. The finding that code-execution frequency—not search frequency—drives accuracy is a concrete empirical result about harness design choices (tool mix, turn budget, feedback granularity) that generalizes to other tool-augmented agent harnesses. The harness also exemplifies automated, ground-truth-verified evaluation loops where the environment (compiler) replaces human or model judges, a design pattern increasingly relevant for meta-harness pipelines that need scalable correctness signals. The cost/latency breakdown per model provides a practical resource-allocation template for anyone building multi-model evaluation harnesses.