h1: A Taste of the Bitter Lesson in Automated Theorem Proving

Skander Moalla; Ahmad Rammal; Niket Patel; Remi Munos; Julia Kempe

cs.LGOct 25, 2026

h1: A Taste of the Bitter Lesson in Automated Theorem Proving

Authors: Skander Moalla, Ahmad Rammal, Niket Patel, Remi Munos, Julia Kempe

Organizations: FAIR at Meta · EPFL · CERMICS, ENPC, Institut Polytechnique de Paris · New York University

Abstract

While progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models, formal theorem proving has increasingly relied on human-designed workflows around these models, such as planning, decomposition, and orchestrating specialized provers. This raises a bitter-lesson question: can a simple agentic loop that scales test-time compute match these workflows? The answer matters as formal verification must scale to keep up with frontier models producing research mathematics, yet new workflows rarely settle it, as their gains are often confounded with stronger models or more compute. We study this question with h1, a simple harness that gives a model an efficient interface to Lean 4 and keeps it working through verifier feedback and self-reflection, without imposing a decomposition or search structure. h1 reaches state-of-the-art results on PutnamBench, FATE-X, and FormalConjectures100-Solved, settles eight open problems in FormalConjectures, and, at matched models, matches or outperforms specialized workflows such as Goedel-Architect and AlphaProof Nexus, surprisingly showing that a single attempt (pass@1) can often scale to solve open problems. Through ablations and matched-model comparisons with Claude Code and AxProverBase, we find that simplicity alone is not enough: an efficient Lean interface largely determines cost and solve rate. We thus recommend that future work evaluate frontier models with efficient execution feedback before prescribing workflows, at the risk of bitter lessons.

Figures & tables

Figure 1: (Left) Simple scaling Pareto-dominates specialized systems. On PutnamBench (672 competition problems), h1 with DeepSeek V4 Flash Pareto-dominates Goedel-Architect’s best of four runs (pass@4) seeded with natural-language proofs. With GPT-5.5, it solves every solvable problem, as Humanfia and Aleph Prover do, at lower cost. (Middle) Longer attempts can outperform repetition. On five open Erdős problems, a single h1 attempt (pass@1) beats three attempts of AlphaProof Nexus’s basic agent (APN basic, pass@3) at lower mean cost per success, can be cheaper than repeating h1 itself, and Pareto-dominates the full APN system. (Right) Simple harness design is important for scaling efficiency and effectiveness. On a 100-problem PutnamBench subset, Gemini 3 Flash trails Opus 4.5 in the AxProverBase loop but overtakes it in h1 at matched budget through more efficient tool use and caching.

Panel of Figure 2 — Figure 2: h1 : a simple harness that scales. An LLM agent edits a Lean file through reasoning and tool calls (ReAct; Yao et al., 2023 ) until it submits or reaches the $T$ -turn limit, forcing submission. An external validator then checks the proof. On failure, a reflection LLM compacts the transcript and feedback for the next iteration. The loop provides Lean tools without prescribing a proof search structure. Search uses LeanExplore ( Asher, 2025 ) , Loogle ( Breitner, 2023 ) , and grep; proof fragments run in the Lean read–eval–print loop (REPL) ( leanprover-community, 2023 ) ; the language server (LSP) reports goals and definitions; SafeVerify ( GasStationManager, 2024 ) performs validation.

Figure 3: Generalist models reach frontier results through simple scaling. On FC100-solved (left) and FATE-X (right), increasing h1 ’s inference budget takes generalist models beyond published benchmark scores. On FC100-solved, h1 with Gemini 3.1 Pro matches the DeepMind (DM) prover agent’s score at a quarter of its budget cap; with GPT-5.6 Sol, it solves 78, and 90 on FATE-X. With DeepSeek V4 Flash, h1 surpasses AlphaProof on FC100-solved and Leanstral 1.5 on FATE-X. Baseline markers show the best published results as of August 27, 2026.

Problem	Statement proved
Erdős 138, variant	$W(k)/2^{k}\to\infty$ for the two-colour van der Waerden number
Erdős 337, variant	$\|(A+A)\cap[2N]\|/\|A\cap[N]\|\to\infty$ for thin asymptotic bases (Ruzsa–Turjányi)
OEIS A108081	$\|x_{n}\|=a(n-1)$ for the inductively defined words
OEIS A211417	$a(p^{k})\equiv a(p^{k-1})\pmod{p^{3k}}$ for primes $p\geq 5$
OEIS A022030	$a(n)=4a(n-1)-a(n-3)+a(n-4)$ for $n\geq 4$
Open Quantum Problem 35	an AME $(9,10)$ state exists

Table 1: Eight problems marked as open in Formal Conjectures proved by h1 with GPT-5.6 Sol.

Benchmark	System + model	Time cap	Solved	Cost
Putnam 2025 (Numina formalization)	Numina, no informal prover, Opus 4.5	–	4/12	–
	h1 + Opus 4.5	–	7/12	$1,429 total
	Numina, full system, Opus 4.5 + Gemini 3 Pro + GPT-5.2	–	12/12	$1,800 cap
	h1 + GPT-5.2	–	12/12	$565 total
PutnamBench’s 2025 slice	h1 + Opus 4.7	–	11/12	$25.97/prob.
	MerLean + Opus 4.7	–	12/12	not reported

Table 2: Simple scaling often matches specialized systems, while model progress closes further gaps. Row groups separate matched-model comparisons from those using other models. The 4-hour cap is FormalQualBench’s official limit;

T50

T200

allow 50/200 turns per iteration; /goal lets a small model judge completion. Table 14 adds measured times.

Figure 4: (Left) Detailed prompts sustain progress on open problems. With Gemini 3.1 Pro on six open Erdős problems and a

150 cap per attempt, a single attempt with detailed prover and reflection prompts, which among other things deflect giving up and cheating, outperforms six attempts with brief ones. (Right) Moderate numbers of turns between reflections outperform both extremes. Solves with Gemini 3 Flash on Putnam100 (

20 cap) and Gemini 3.1 Pro on FATE-X ($50 cap) as the number of turns between reflections varies.

Appendix figures & tables41 assets

Supplementary material from the paper’s appendix.

Appendix

Tool and arguments	Behavior
view_working_file (offset, limit \| None)	Line-numbered, paginated view of the mutable file; 40,000-byte view limit.
view_original_file (offset, limit \| None)	The immutable statement file with its initial compile feedback; 40,000-byte view limit.
edit_working_file (old_string, new_string, replace_all)	Whitespace-tolerant replacement; unique unless replace_all . Compiles after editing and returns errors and open goals (32,000 characters). Invalid import edits are rolled back.
undo_edit_working_file ()	Revert the last edit and recompile; compiler feedback: 32,000 characters.
submit_working_file (updated_file, reasoning)	Check for errors and unfinished goals, then compile and validate with SafeVerify in an isolated environment; ends the iteration.
lean_leanexplore (query)	Natural-language search over Mathlib declarations (LeanExplore; Qwen3 embedding and reranker); 6 results with name, module, signature, description.

Appendix

Table 3: Tools available to h1 . File tools let the multi-turn LLM inspect, edit, and submit its proof. Search tools retrieve Mathlib declarations; the REPL checks standalone Lean snippets; language-server tools expose goals, diagnostics, and symbol information.

Prompt version	Multi-turn LLM	Reflection LLM
Brief	“Prove the Lean file in the user message. Use the available tools and submit your completed working file.”	“Summarize the prover’s progress for its next attempt. Be concise and return only the summary.”
Detailed	Describes tool use and iterative state; specifies statement integrity, proof-validity and disproof requirements, and persistence. Includes general advice and examples.	Instructs faithful context compaction: preserve verified progress and useful lemma names, attribute unverified claims to the multi-turn LLM, and treat incomplete submissions as checkpoints.

Appendix

Table 4: Brief and Detailed system prompts. Each LLM independently uses either version, giving four prompt combinations. Detailed prompts include general advice and examples without imposing a fixed search structure or decomposition procedure. Tool descriptions are included only when the corresponding tool is available.

Observed failure	Prompt response
The multi-turn LLM uses the Lean REPL like a shell to hunt through the sandbox filesystem for a stored solution	The sandbox contains no solutions. The prompt explains that searching for stored answers or guessing proof names is wasted effort and directs the model to search for supporting lemmas instead.
The reflection LLM treats an incomplete checkpoint as a final failure	The submission tool asks the multi-turn LLM to explain why it is submitting. This reason is passed to the reflection LLM, whose prompt distinguishes a claimed complete proof from a checkpoint submitted when a limit is reached and asks it to preserve partial progress and remaining goals.
The reflection LLM turns an unverified claim into a fact	Attribute mathematical beliefs to the multi-turn LLM; state file contents and verifier feedback directly.
The reflection LLM reinforces a decision to give up	Retain the concrete unresolved obstacle without repeating claims that the problem is impossible or too difficult.

Appendix

Table 5: Observed failures and corresponding instructions in the Detailed prompts.

What goes wrong	What h1 does	What the model sees	How the attempt continues
Lean error or open goal	Keep the edit and check the file.	Lean’s errors and remaining goals.	The model can revise the proof in the same iteration.
REPL connection loss	Restart Lean and repeat the same command once.	The command’s result if it succeeds; otherwise a failure message from the tool.	If the command succeeds, the same model interaction continues.
REPL timeout	Restart Lean without repeating the command that timed out.	A timeout message from the tool.	Edit checks restore the previous file; scratch execution allows one failure. A timeout before submission interrupts the execution.
Process failure during an edit check	Restore the file to its state before the edit and check it after restarting Lean.	A message that the edit was rejected and already undone.	Continue if the restored file checks; otherwise interrupt the execution.
Process failure during scratch-code execution	Leave the working file unchanged. Allow one failure; stop after two in a row.	A warning that the scratch computation ran out of time or memory.	After the first failure, the model can try again. A second consecutive failure interrupts the execution.
Initial health check fails	Stop if Lean cannot check the original file before proving begins.	Nothing: no model call has been made.	Proving can begin once the Lean service is working.

Appendix

Table 6: How h1 handles Lean errors and process failures. Proof errors are returned to the model for revision. Process failures trigger a restart or end the current execution, depending on where they occur. Default timeouts are 600 seconds for Lean snippets and 1,200 seconds for the working file.

Benchmark	Source revision	Lean	Mathlib
PutnamBench (including Putnam100 and the 2025 slice)	3c9b9268 (2026-07-23)	4.27.0	4.27.0
FATE-X	a6fb49ee (2026-02-23)	4.28.0	4.28.0
FormalQualBench	efaa113c (2026-03-19) ∗	4.28.0	4.28.0
FC100-solved	7862bf6a (2026-04-29)	4.27.0	4.27.0
Erdős problems (APN comparison)	7862bf6a (2026-04-29)	4.27.0	4.27.0
Putnam 2025 (Numina)	60d33c8b (2026-01-20)	4.26.0	4.26.0

Appendix

Table 7: Benchmark sources and Lean environments. Source revisions and Mathlib releases follow the setup recipes; Lean versions are cross-checked against run metadata. Dates are source commit dates.

Stage	Check
Trusted challenge	Compile the original statement with fixed Lean and library versions in an isolated environment; retain its compiled artifact in storage inaccessible to the prover.
Submission compile	Compile the submitted source in a separate, fresh, networkless sandbox against read-only dependencies, preserving the module’s relative path.
Kernel validation	Compare the original and submitted compiled artifacts using SafeVerify in a trusted Lean project. Accept only when the verifier reports success and exits without error.
Proof or disproof	Accept a proof of the target theorem. Where disproofs are enabled, also accept a .disproof declaration proving the supported negation of that theorem.

Appendix

Table 8: Independent validation of submitted source. The same boundary applies to API provers and coding agents. Only the designated source file crosses from the agent workspace into validation; the agent’s compiled artifacts are never trusted.

Model and configuration	Input	Cache read	Cache write		Output
			5 min	1 hour
Claude Haiku 4.5	1.00	0.10	1.25	2.00	5.00
Claude Opus 4.5, 4.6, 4.7, 4.8	5.00	0.50	6.25	10.00	25.00
Gemini 3 Flash	0.50	0.05	–	–	3.00
Gemini 3.1 Pro ( $\leq$ 200k input tokens)	2.00	0.20	–	–	12.00
Gemini 3.1 Pro ( $>$ 200k input tokens)	4.00	0.40	–	–	18.00

Appendix

Table 9: Reference token prices, in US dollars per million tokens. Public API prices are reported by Artificial Analysis (accessed September 24, 2026); GPT-5.6 Sol retains its July 9 launch rates . Leanstral uses Mistral Small 4 as a pricing proxy; DeepSeek uses the fixed April 26, 2026 reference card described in Appendix C.5 . Input denotes uncached input; cache reads and writes are counted separately. The cache-write columns distinguish five-minute and one-hour retention; a dash denotes no separate charge in our accounting. Gemini 3.1 Pro’s input-length tier applies to the entire call. Reasoning tokens count as output. Reported curves and costs retain the experimental price cards. Costs quoted from other studies retain their reported accounting.

System / model	Setting	Solved (%)	$/problem
Ours + GPT-5.5	Capped	87.5	5.28
	Capped	95.5	6.63
	Endpoint	99.7	9.17
	+ 8 attempts	100.0	17.86
Ours + DeepSeek V4 Flash	Capped	69.5	0.40
	Capped	75.6	0.46

Appendix

Table 10: PutnamBench results underlying Figures 1 (left) and 6 . Solve rates use 672 problems except Hilbert (462/660, 70.0%), DeepSeek V4 Flash with TIR (109/200, 54.5%), and Aleph’s first result (500/660, 75.8%). The figure places Hilbert and TIR at equivalent rates on its 672-problem axis; Aleph’s first point retains its published count of 500. Dollar values are per-problem means unless qualified above; Hilbert’s cost is an attributed estimate, and TIR reports no cost. Our DeepSeek values are estimated API-equivalent costs.

Model / harness	PutnamBench	FC100-solved	FATE-X
DeepSeek V4 Flash (estimated)	92.26%	96.38%	96.15%
GPT-5.5	79.09%	–	–
GPT-5.6 Sol	–	93.77%	96.21%
Gemini 3.1 Pro	55.39%	61.21%	69.96%
Claude Opus 4.5	–	–	91.64%
Claude Opus 4.8	–	–	91.50%

Appendix

Table 11: Fraction of input tokens read from cache. DeepSeek values are reconstructed estimates; others use provider-reported counters. Models use h1 unless stated otherwise. A dash denotes no listed run; n.r. means no cache-read counters were recorded.

Target	Theorem proved
Erdős 138, variant dvd_two_pow	Let $W(k)$ be the two-colour van der Waerden number, the least $N$ such that every two-colouring of $\{1,\dots,N\}$ contains a monochromatic $k$ -term arithmetic progression. Then $W(k)/2^{k}\to\infty$ . Erdos138_dvd_two_pow_solution.lean
Erdős 337, variant ruzsa_turjanyi	For every asymptotic additive basis $A\subseteq\mathbb{N}$ of density zero, that is with $\|A\cap[1,N]\|=o(N)$ , the ratio $\|(A+A)\cap[1,2N]\|\,/\,\|A\cap[1,N]\|$ tends to infinity. Erdos337_ruzsa_turjanyi_solution.lean
OEIS A108081	Let $X$ be the smallest set of words over $\mathbb{Z}$ containing $[0]$ and closed under $(u,v)\mapsto l(u)\,v$ and $(u,v)\mapsto u\,r(v)$ , where $l$ and $r$ reverse a word and shift its letters by $-1$ and $+1$ . For every $n\geq 1$ , the number of words of length $n$ in $X$ equals $a(n-1)$ , where $a(n)=\sum_{k=0}^{n}\binom{n+k-1}{k}F_{n-k+1}$ . OeisA108081_count_words_in_x_is_a_shifted.lean
OEIS A211417	For $a(n)=(30n)!\,n!\big/\bigl((15n)!\,(10n)!\,(6n)!\bigr)$ , every prime $p\geq 5$ and every $k\geq 1$ satisfy $p^{3k}\mid a(p^{k})-a(p^{k-1})$ (Bala’s supercongruence). OeisA211417_supercongruence_solution.lean
OEIS A022030	Let $a(0)=4$ , $a(1)=16$ and, with truncated division, $a(n+2)=\bigl(a(n+1)^{2}+a(n)-1\bigr)/a(n)-1$ for even $n$ and $a(n+2)=a(n+1)^{2}/a(n)+1$ for odd $n$ . Then $a(n)=4a(n-1)-a(n-3)+a(n-4)$ for every $n\geq 4$ . OeisA22030_conjecture.lean
Open Quantum Problem 35, ame_9_10_open	There exists a unit vector $\psi\in\left(\mathbb{C}^{10}\right)^{\otimes 9}$ whose reduced density matrix on any four of the nine parties is the maximally mixed state; that is, an AME $(9,10)$ state exists. OpenQuantumProblem35_ame_9_10_open_solution.lean

Appendix

Table 12: Eight Formal Conjectures targets proved by h1 . Each row states the result proved in the corresponding Lean file, listed beneath it. † The distributed statement was repaired before it was proved: Conjecture 100 took the degree norm of

G

rather than of its complement, and Conjecture 314 used a different induced-path invariant.

Target	Defect	Correction or scoring decision
Erdős 507	Signed triangle area and repeated vertices do not express the intended minimum nonnegative area of three distinct points.	Proofs of the original targets do not establish the intended geometric result.
Green 16	One natural-number answer is used for every $N$ , although the extremal quantity depends on $N$ .	Define the extremal function of $N$ and state the asymptotic bound.
Erdős 566/567	The size Ramsey number counts edges of an arbitrary host, whereas the source asks for the ordinary Ramsey number.	Use the least number of vertices of a complete host.
Lam–Litt	A chosen denominator can vanish at the initial point, making the cleared-denominator identity degenerate.	Require that denominator to be nonzero at the initial point.
Written on the Wall II, 100/160/314	The extraction loses a complement, substitutes a cycle count for a binary indicator, or uses average distance for induced-path length.	Restore the complement-degree norm, the $C_{4}$ -free indicator, and the largest induced-path order, respectively.
Open Quantum Problem 13	Editable answers do not fix the proposed maximum number of mutually unbiased bases.	State the fixed dimension-six conjecture IsMaxMUBCount 6 3 .

Appendix

Table 13: Statement defects and benchmark repairs. Repairs here refer to our benchmark statements, rather than the status of the upstream repository. A repair does not imply that the repaired problem was solved: among these rows, Written on the Wall II Conjectures 100 and 314 contribute to Table 12 . Editable-answer defects can coexist with a mathematical misformalization.

Benchmark	System + model	Time cap	Solved	Cost	Time
Putnam 2025 (Numina formalization)	Numina, no informal prover, Opus 4.5	–	4/12	–	–
	h1 + Opus 4.5	–	7/12	$1,429 total	6,122 min
	Numina, full system, Opus 4.5 + Gemini 3 Pro + GPT-5.2	–	12/12	$1,800 cap	3,889 min
	h1 + GPT-5.2	–	12/12	$565 total	9,636 min
PutnamBench’s 2025 slice	h1 + Opus 4.7	–	11/12	$25.97/prob.	694 min
	MerLean + Opus 4.7	–	12/12	not reported	789 min

Appendix

Table 14: Full comparison including measured times. The results of Table 2 , with the Time column retained. Cap denotes the time limit; Time reports measured time, summed across problems for Putnam and IMO and averaged over successes for FormalQualBench.

Figure 5: Claude Code improves with our Lean tools but still falls short of h1 on the PutnamBench subset. With Opus 4.8, native Claude Code solves 81 problems; our prompt and Lean tools through MCP, in place of its built-in shell and file tools, raise this to 95, while h1 reaches 99. The FATE-X comparison appears in Figure , right.

Figure 6: Reflection substantially improves h1 ’s coverage, exceeding Goedel-Architect’s pass@4 coverage at lower estimated cost. With the same DeepSeek V4 Flash model, h1 also substantially outperforms Goedel-Architect’s tool-integrated reasoning (TIR) baseline, showing that its baseline understates what a simple agent can achieve.

Figure 7: Figure 3 with the DeepSeek V4 Flash setting labelled. FC100-solved (left) and FATE-X (right); the DeepSeek V4 Flash runs use h1 without self-reflection.

Figure 8: The five Erdős problems in Figure 1 (middle), plus Erdős 125. Solid coloured curves vary the active-time cutoff within an attempt, separately for each pass@

k

; filled circles mark terminal results. The dashed connection between those circles shows repetition at the final allowance. Grey circles are APN basic’s published pass@

k

points, and the hollow diamond is APN full’s pass@1. All use Gemini 3.1 Pro. Horizontal scales differ across panels. Following AlphaProof Nexus ( Tsoukalas et al., 2026 ) , we report cost conditional on success. All 16 h1 replicas on Erdős 125 ended in Lean REPL timeout errors, so its conditional cost is undefined. Errors count as failures. APN full also uses AlphaProof, whose cost is absent from the published coordinates.

Figure 9: Per-problem success under different prompts for the two LLM roles. The same runs and $150 cap as Figure 4 ; bars show pass@1, with all replicas in the denominator.

Figure 10: Model scaling on six Erdős problems with detailed instructions. All models use a

300 per-attempt cap. Curves sum per-problem pass@

k$ estimates; Gemini 3.1 Pro has 16 replicas, GPT-5.4 nine, and Opus 4.6 ten.

Figure 11: Per-problem success for the model comparison. Bars show pass@1 in the runs of Figure 10 , with detailed instructions for both LLM roles and a $300 per-attempt cap.

$k$	h1 (%)	APN basic (%)	APN full (%)
1	68.75	35.67	71.67
3	79.73	63.36	–
6	82.90	76.14	–
10	83.33	81.82	–

Appendix

Table 15: Success rates across all six Erdős problems. Each entry is

100/6

times the sum of the six per-problem pass@

k

estimates, giving every problem equal weight. For h1 , each estimate is

1-\binom{16-c_{i}}{k}/\binom{16}{k}

, where

c_{i}

is the number of accepted replicas; all errors count as failures, including all 16 on problem 125. APN columns average the published per-problem rates with the same weights. These are terminal outcomes, not matched-budget estimates.

Figure 12: Longer h1 attempts can be cheaper than repetition even when failures are charged. All curves use Gemini 3.1 Pro in the same harness. Lines join nondominated observed points as the per-attempt dollar cap varies; circles mark terminal results. Cost averages successful and unsuccessful groups, with cancellation at the first accepted proof in successful groups. Left: the five-problem subset used in Figure 1 . Right: all six problems, including Erdős 125 with zero accepted attempts and its recorded costs. Its unconditional mean cost remains defined even with no successful attempts, whereas its conditional cost is undefined. Solve rates and costs give each problem equal weight.

Figure 13: The trade-off between longer attempts and repetition varies by problem. The same unconditional-cost calculation as Figure 12 , shown separately for each of the six Erdős problems. Lines join nondominated observed points; circles mark terminal results. All groups contribute to cost, including those that terminate in errors. Horizontal scales differ across panels. On Erdős 152, pass@10 reaches 87.5% at

483 and leads the tested smaller values of

until pass@6 reaches 94.2% at

535.

Figure 14: Dollar and time alignment give the same terminal comparisons. Both panels average the same five problems equally and count each group’s cost up to its first eligible proof. Only the common allowance across problems changes. Solid curves vary that allowance at fixed

k

; circles mark terminal results. APN’s published points are identical in both panels.

Figure 15: The most economical model depends on the target solve rate. On the PutnamBench subset, Leanstral 1.5 supplies the frontier through 72 solves and Gemini 3.1 Pro extends it to 99, while Gemini 3 Flash lies below their combined frontier. Each curve varies the per-problem cap; cost averages all 100 problems, including failures. Dots mark full-run endpoints. Leanstral costs are API-equivalent estimates using a measured 65% average cache rate at maximum context length.

Figure 16: h1 overtakes AxProverBase as the budget grows across the six settings in Figure . AxProverBase is shown both before and after screening out proofs using native_decide ; overlapping lines indicate no screened solves. All h1 solves pass external validation.

Figure 17: Cost per problem by token type, PutnamBench subset, nine model settings under AxProverBase (AxP) and h1 . Bars average costs across solved and unsolved problems. Percentages show output tokens’ share of total cost.

Figure 18: PutnamBench subset solve rates for h1 and AxProverBase as the budget increases. h1 with Opus 4.5 solves 61 problems at the $20 per-problem cap.

Figure 19: Bad imports consume proof-checking attempts. The fraction of failed builds whose first Lean error is a bad import is 42.2% for AxProverBase with Gemini 3 Flash and 0.6% with Opus 4.5; dashed lines show the paper’s reported 56% and 0.4%. h1 seeds the working file with import Mathlib and records no such failures.

Figure 20: Model releases and benchmark dates. Benchmark dates marked ∗ are first benchmark-containing commits, not verified public-release dates; FC100 uses the tagged benchmark release. Dates distinguish possible exposure to statements, formalizations, and published solutions; they do not establish the contents of proprietary training data.

Figure 21: Tools provide overlapping benefits. Individual search tools or the REPL recover most of the full tool set’s gains; removing any single tool has little effect on coverage. Results cover the PutnamBench subset with Gemini 3 Flash and FATE-X with Gemini 3.1 Pro.

Figure 22: The detailed prompt improves solve rates on both ablation settings. Gemini 3 Flash on the PutnamBench subset (

20 per problem) and Gemini 3.1 Pro on FATE-X (

50); all 100 problems per arm remain in the denominator, including crashes. The prompt variants are specified in Appendix B.2 .

Figure 23: The two reflection LLM inputs yield similar solve counts in these runs. Full transcript versus distilled final attempt: 69 versus 67 solves on the PutnamBench subset with Gemini 3 Flash, and 63 versus 64 on FATE-X with Gemini 3.1 Pro. The per-problem caps are

20 and

50, respectively, including prover and reflection LLM calls; each arm contains 100 problems and one run.

	Putnam100			FATE-X
Cost component	Full	Distilled	Change [95% CI]	Full	Distilled	Change [95% CI]
Reflector input	0.91	0.04	$-95.1\%$ [ $-95.6,-94.6$ ]	1.74	0.18	$-89.6\%$ [ $-90.9,-88.2$ ]
Reflector output	0.10	0.38	$+260.4\%$ [ $+217.7,+311.1$ ]	0.92	0.69	$-24.2\%$ [ $-35.5,-11.5$ ]
Prover calls	7.99	8.75	$+9.6\%$ [ $-0.1,+20.0$ ]	23.37	25.09	$+7.3\%$ [ $+1.1,+14.3$ ]
Total	9.00	9.17	$+1.9\%$ [ $-6.9,+11.5$ ]	26.02	25.96	$-0.2\%$ [ $-6.0,+6.1$ ]

Appendix

Table 16: Lower input costs for reflection are offset by higher prover-call costs. Mean dollars per problem with full transcript versus distilled final attempt. Relative changes compare mean costs; brackets give 95% percentile intervals from 50,000 paired bootstrap samples of problems.

Figure 24: Solve rates under different tool configurations and inference budgets. Gemini 3 Flash on the PutnamBench subset (

20 per problem; left) and Gemini 3.1 Pro on FATE-X (

50; right). The working-file baseline permits editing and checking the proof file. Blue curves add one of five capabilities: semantic, type, or text search, the Lean REPL, or the language server. Pale curves remove one capability from the complete tool set. The working-file baseline generally solves fewer problems; the other configurations substantially overlap. On the PutnamBench subset, all tools retain all 49 working-file-baseline solves and add 20; on FATE-X, they retain 48 of 49 and add 15.

Figure 25: Tool use when search and execution capabilities change. Top: median calls to each search tool among problems solved by each configuration; stacked heights sum these tool-specific medians. Bottom: each tool’s median call count when it is the only additional capability, divided by its median with all tools available. These comparisons use each configuration’s own solved problems.

Figure 26: Solve rates at different budgets and reflection intervals. Reflection follows every 1, 10, 50, 100, or 200 proof-search turns (

T1

–

T200

). Gemini 3 Flash is evaluated on the PutnamBench subset at up to

20 per problem (left), and Gemini 3.1 Pro on FATE-X at up to

50 (right). Reflection every turn produces fewer solves over most observed budgets; intervals of 10 and 50 turns give similar curves.

Figure 27: More reasoning per turn can make test-time scaling more efficient. Gemini 3.1 Pro on the PutnamBench subset with low, medium, and high reasoning effort. Curves plot solves against mean cost, including failed attempts; legends report final solve counts and mean costs.

Figure 28: Token use and cost at different reflection intervals. Gemini 3 Flash on the PutnamBench subset (top) and Gemini 3.1 Pro on FATE-X (bottom). Left: input, cached input, and output tokens averaged over recorded problems. Middle: the fraction of all input tokens served from cache. Right: mean inference cost per problem, including failed attempts, split by token type; numbers above bars give solve counts. Calls to both the multi-turn LLM and reflection LLM are included. The horizontal axis gives the maximum number of proof-search turns between reflections.

Figure 29: Time to acceptance and accepted-file length. The selected runs contain 670/672 accepted PutnamBench problems with GPT-5.5, and 90/100 on FATE-X, 14/23 on FormalQualBench, and 78/100 on FC100-solved with GPT-5.6 Sol: 852 accepted proofs in 895 attempts. Left: active hours to first acceptance. Right: total lines in the accepted Lean file. Densities are estimated in

\log_{10}

space and normalized so their area in that space equals the benchmark’s acceptance percentage. Dashed lines mark medians among accepted proofs.

Figure 30: Cumulative distributions of time to acceptance and accepted-file length. The runs are those in Figure 29 . Counts are divided by all attempted problems, so each curve ends at the run’s acceptance percentage. Diamonds mark medians among accepted proofs.

Figure 31: Search time and total file length across 852 accepted proofs. GPT-5.5 on PutnamBench; GPT-5.6 Sol on FATE-X, FormalQualBench, and FC100-solved.

Large Language Model-Guided Theorem Proving

See all 46 papers

Jun 8, 2026

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics

LLMs have recently achieved strong results on formal proving benchmarks. However, existing evaluations remain heavily concentrated on competition-style problems and often fail to capture how models behave on longer, more dependency-rich mathematical developments. We introduce TheoremBench, a Lean4 benchmark designed to evaluate theorem provers beyond contest settings. The benchmark is built from nearly one hundred classical theorems and is released in two complementary forms: a plain main version containing one target theorem per instance, and a premised version that expands each theorem into a structured family of related proving tasks consisting of the main theorem together with automatically extracted supporting subtheorems. This design enables evaluation of not only whether the final theorem was proved from scratch, but also of partial progress through the internal proof structure of a theorem. Our experiments show that explicit premises substantially improve performance for Lean4-capable prover models. To provide a comprehensive evaluation, we introduce theorem-level coverage and token-efficiency metrics that expose qualitative differences in proof behavior. The results show that current provers remain strongly biased toward easy subtheorems and often solve theorems through long and inefficient tactic traces rather than compact proof plans. TheoremBench therefore provides a more fine-grained view of formal reasoning ability and highlights the importance of structural benchmark design for evaluating Lean4 theorem provers.

QuocViet Pham, Elvir Karimov, Andrey Galichin +1

Skolkovo Institute of Science and Technology · HSE University · Sberbank +1

Mathematical Reasoning Benchmarks LLM Evaluation Automated Theorem Proving Benchmark Design Lean Theorem Proving Large Language Model-Guided Theorem Proving

Ask PDF

May 26, 2026

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

MerLean-Prover is an end-to-end Lean4 theorem prover that replaces sorry declarations with kernel-checkable proofs. It is built from three agent types (Planning, Check, and Lean) composed by a recursive outer loop whose unit of revision is the proof plan itself, and uses no fine-tuning, no custom RL objective, and no theorem-specific scaffolding. On FormalQualBench, a benchmark of 23 PhD-qualifying-exam theorems, MerLean-Prover solves 10/23, surpassing the strongest published open-source baseline (OpenGauss, 8/23). On Putnam2025, the same harness closes 12/12 with substantially lower total wall-clock than the next-best system that closes the full set. The harness also transfers to smaller models: Sonnet closes all four tested FormalQualBench problems, and Haiku closes the two short ones. These results suggest that harness design is a central factor in end-to-end Lean4 theorem proving, alongside raw model capability, and that a relatively simple harness can already be effective.

Jinzheng Li, Zeru Zhu, Yuanjie Ren

1Northeastern University · 2Stony Brook University · 3Massachusetts Institute of Technology

Large Language Model-Guided Theorem Proving Automated Theorem Proving Lean Theorem Proving

Ask PDF

Jun 2, 2026

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks

Large Language Models (LLMs) exhibit strong informal mathematical reasoning but struggle to generate mechanically verifiable proofs in formal languages like Lean. We present LEAP, an agentic framework that enables general-purpose foundation models to achieve state-of-the-art performance on automated formal theorem proving. LEAP leverages foundation model capabilities, such as informal reasoning, instruction following, and iterative self-refinement. By decomposing complex problems into smaller units, the system bridges formal proof construction with informal blueprints through continuous interaction with the Lean compiler. To provide a rigorous evaluation beyond increasingly saturated benchmarks, we introduce Lean-IMO-Bench, a benchmark of IMO-style problems formalized in Lean, with short statements yet highly non-routine and multi-step proofs across a wide range of difficulty levels. Empirically, on the latest 2025 Putnam Competition, an annual mathematics competition for undergraduate students in North America, LEAP solves all 12 problems, matching recent breakthroughs by frontier formal mathematical models. On Lean-IMO-Bench, LEAP boosts the one-shot formal solve rate of general-purpose LLMs from below 10% to 70%, notably surpassing the 48% benchmark set by a specialized, gold-medal-caliber IMO system. Furthermore, we demonstrate LEAP's research-level utility by autonomously formalizing complex proofs for open combinatorial challenges, including a verified proof for a key subproblem in Knuth's Hamiltonian decomposition of even-order Cayley graphs.

Po-Nien Kung, Linfeng Song, Dawsen Hwang +10

Google Cloud AI Research · Google Cloud · Google DeepMind

Mathematical Reasoning Benchmarks Large Language Model-Guided Theorem Proving Automated Theorem Proving Interactive Theorem Proving Lean Theorem Proving

Ask PDF

Abstract

Large Language Model-Guided Theorem Proving

Explore similar work

TheoremBench: Evaluating LLMs on Theorem Proving in Formal Mathematics

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving

LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks