FormalMATH

Overview

FormalMATH expands formal theorem-proving evaluation in two directions at once. Its 5,560 Lean 4 statements are 22.8 times the size of MiniF2F's 244-problem test set, and the source mathematics ranges from high-school Olympiad problems to undergraduate integration, differentiation, multivariable calculus, algebra, and sequences. A prover receives a formal theorem statement with a proof hole and must produce code that Lean accepts.

Constructing a large benchmark is difficult because compilation checks syntax, not semantic fidelity to the original problem. The authors first train autoformalizers on 9,260 compile-checked pairs, then sample candidates from multiple models. Candidates pass through the Lean compiler, unanimous semantic review by several general-purpose LLMs, negation-based attempts to disprove the statement, and finally review by 12 Olympiad-medalist-level experts. The expert stage retains 72.09% of what reaches it and costs an average of $6.89 per statement over 22 days.

The paper evaluates two fundamentally different prover families. Single-pass systems emit a complete proof trajectory; best-first systems inspect intermediate proof states and expand candidate tactics. Because 32 complete samples are not equivalent to a 1 × 32 × 100 tactic-search budget, TokenWave's leaderboard includes only full-set single-pass Pass@32 rows. Search results remain part of the paper's analysis but do not determine rank here.

Why it matters

Formal proof benchmarks can saturate while still covering a narrow slice of mathematics. MiniF2F concentrates on high-school algebra and number theory, while ProofNet is small and undergraduate-focused. FormalMATH's size and split domain structure make it harder for a prover to hide a training bias behind one aggregate success rate.

The construction pipeline is also part of the benchmark's value. A compiling but mistranslated theorem makes proof generation easier or tests the wrong claim. Multi-model semantic checks, attempted disproof, and expert review are defenses against that silent failure, and the reported preservation funnel makes the cost of each defense inspectable.

Contributions

• Releases 5,560 formally verified Lean 4 theorem statements across high-school and undergraduate mathematics, 22.8 times the size of MiniF2F's 244-problem test set.
• Introduces a human-in-the-loop construction pipeline combining multi-model autoformalization, compiler validation, multi-LLM semantic checking, negation-based disproof, and expert review.
• Provides full-benchmark evaluations for single-pass and search-based theorem provers, plus a 425-problem FormalMATH-Lite subset for controlled test-time-scaling studies.
• Documents domain imbalance, diminishing returns from large sampling budgets, overuse of automation tactics, and differences among vanilla, naive-CoT, and natural-language-augmented proof generation.

Method & evaluation

• Natural-language problems are collected from high-school sources such as Omni-MATH and BlueMO and undergraduate sources such as U-MATH, HARDMath, and DEMI-MathAnalysis. The final 5,560 statements cover distinct high-school and undergraduate domain taxonomies.
• A compile-and-filter stage first produces 9,260 natural-language/Lean statement pairs for fine-tuning specialized autoformalizers. Multiple autoformalizer models then sample candidate statements with best-of-N generation.
• Every candidate must type-check in Lean 4. Surviving statements are back-translated and compared with the source problem by multiple general-purpose LLMs; only unanimous semantic approvals continue to negation-based disproof with theorem provers.
• Twelve Olympiad-medalist-level experts perform the final semantic check. Manual review costs an average of $6.89 per statement over 22 days and retains 72.09% of the candidates that reach this stage, yielding 21.7% of the original natural-language pool.
• A proof is successful only if Lean accepts it. Single-pass systems sample complete proofs, while best-first systems expand tactics over N search attempts, S tactics per expansion, and T expansion steps; their budgets are therefore reported separately.
• The HTML leaderboard uses the five full-set single-pass generation rows at Pass@32. BFS-Prover and InternLM-Prover are excluded because their 1 × 32 × 100 search budgets are not equivalent to 32 complete proof samples.

Evaluation metrics

Full-set Pass@32 (%) — Higher is better. Percentage of all 5,560 statements for which at least one of 32 independently generated complete proofs is accepted by Lean; used for the displayed single-pass leaderboard. Score range: [0, 100].

Best-first Pass@N×S×T — Higher is better. Success rate for search-based provers with N search attempts, S tactics proposed per expansion, and T expansion iterations; reported separately from single-pass Pass@K. Score range: [0, 100].

FormalMATH-Lite Pass@K — Higher is better. Pass@K on a stratified 425-problem subset (359 high-school and 66 undergraduate problems) used for budgets up to 3,200 complete samples and larger search budgets. Score range: [0, 100].

Leaderboard

All displayed rows use the full 5,560-problem benchmark, single-pass complete-proof generation, and 32 samples. Search-based BFS and InternLM results in Figure 2a use a different 1 × 32 × 100 tactic-search budget and are intentionally not mixed into this ranking.

#	Model	Full-set Pass@32 (%)
1	Kimina-Prover-7B	16.46
2	STP-Lean	13.87
3	Goedel-Prover	13.53
4	DeepSeek-Prover-V1.5-RL	10.18
5	DeepSeek-Prover-V1.5-SFT	8.97

Reading the results

Kimina-Prover-7B leads the directly comparable full-set single-pass setting at 16.46% Pass@32. STP-Lean scores 13.87% and Goedel-Prover 13.53%, only 0.34 points apart. Kimina's margin over second place is 2.59 points, but the more consequential observation is that the strongest prover fails to find any accepted proof for more than five out of six statements even after 32 samples.

DeepSeek-Prover-V1.5-RL reaches 10.18%, compared with 8.97% for its SFT counterpart, an absolute gain of 1.21 points. The paper contrasts that modest improvement with stronger gains from self-play and expert iteration, while cautioning that all methods operate at low absolute success rates on the full set.

The aggregate conceals large domain gaps. The paper reports Goedel-Prover at 50% on undergraduate algebra but 5.21% on calculus and 0% on discrete mathematics under its analysis setting. FormalMATH-Lite experiments also show diminishing returns: increasing STP from Pass@32 to Pass@3200 raises accuracy by only 4.58 points. More sampling helps, but it does not repair missing domain coverage or brittle formal reasoning by itself.

Figures & tables

← Back to Research