A Taste of the Bitter Lesson in Automated Theorem Proving

Summary (Overview)

Core question: Can a simple agentic loop that scales test-time compute match specialized, human-designed workflows for automated theorem proving (ATP) in Lean 4?
Main contribution: The authors introduce h1, a simple harness providing an efficient Lean 4 interface with verifier feedback and self-reflection, imposing no decomposition or search structure.
Key results: h1 achieves state-of-the-art results on PutnamBench, FATE-X, and FormalConjectures100-Solved, settles eight open problems in Formal Conjectures, and at matched models matches or outperforms specialized workflows like Goedel-Architect and AlphaProof Nexus.
Critical finding: A single attempt (pass@1) with extended budget can outperform repetition (pass@k), and harness design details (efficient interface, persistence, context management) largely determine cost and solve rate.
Bitter lesson applied: Simple test-time scaling with frontier models often Pareto-dominates specialized workflows, suggesting future work should evaluate frontier models with efficient execution feedback before prescribing workflows.

Introduction and Theoretical Foundation

The paper is grounded in Sutton's Bitter Lesson (Sutton, 2019), which predicts that general methods scaling with computation ultimately outperform approaches built around human domain knowledge.

The tension: While informal mathematics progress comes from scaling frontier models' chain-of-thought and agentic reasoning, formal theorem proving has increasingly relied on human-designed workflows that orchestrate specialized provers, planning, decomposition, and proof refinement around these models.

Key insight: Formal proof assistants like Lean express mathematical statements in a mechanically checkable language, which naturally supports structured search that can be encoded as workflow harnesses. However, this raises the question: can a simple loop that just provides Lean feedback and sustains work match these complex workflows?

Motivation: The stakes matter because frontier models increasingly generate research mathematics whose informal arguments are difficult to verify. Scaling automated theorem proving to produce mechanically checked proofs is becoming a necessary component of automated discovery.

The confound problem: New workflows are often presented alongside stronger models and more compute, making it unclear whether their gains hold against an efficient simple loop given enough test-time compute.

Methodology

Experimental Setup

Formal proving task: In Lean, the agent must complete a proof in a source file; Mathlib provides shared definitions and proved results. Compilation checks the proof and returns errors, with open goals listing what remains.

Benchmarks (increasing difficulty):

PutnamBench: 672 problems from Putnam competitions (tests efficiency)
Putnam100: 100-problem subset used by AxProverBase
FATE-X: 100 algebra problems at PhD qualifying-exam level
FormalQualBench: 23 theorems at PhD qualifying-exam level
FC100-solved: 100 random Formal Conjectures problems with known informal solutions
Putnam 2025, IMO 2026: Recent problems unseen by models released before them
Open conjectures: Test progress beyond known solutions

Models: Frontier models from OpenAI, Anthropic, Google, plus open-weight DeepSeek V4 Flash and Leanstral 1.5.

Baselines:

Specialized workflows: Goedel-Architect, MerLean, AlphaProof Nexus, OpenGauss, Numina
Simple loops: Humanfia, APN basic, AxProverBase, Claude Code

Cost Measurement

The paper introduces cost per task as a standard metric, noting that prior work rarely compares systems at matched inference compute. Key observation: output tokens can cost up to 100× as much as cached input. Budget $B per problem caps each problem's cost, and solve counts include only verified proofs within budget.

The h1 Harness

h1 operates as a ReAct loop (Yao et al., 2023) with these components:

Iteration structure: The model reasons and calls tools for at most $T$ turns, editing a persistent working file; every edit is compiled and returns errors and open goals.
External validator: Checks the proof against the original statement (via SafeVerify), rejecting placeholders and added assumptions.
Reflection: On failure, a reflection LLM compacts the transcript into verified progress, lessons, and useful lemma names, discouraging giving up (like Reflexion and Self-Refine).
Tools: LeanExplore, Loogle, grep for search; REPL for proof fragments; LSP for goals and definitions; SafeVerify for validation.

Key design principle: No decomposition, planning, or search structure imposed — the model decides how to develop the proof.

Empirical Validation / Results

State-of-the-Art Results

With GPT-5.6 Sol, h1 achieves:

90/100 on FATE-X
78/100 on FC100-solved
14/23 on FormalQualBench
6/6 IMO 2026 problems
670/672 PutnamBench problems with GPT-5.5

Inexpensive models also excel: DeepSeek V4 Flash in h1 solves 43 FATE-X problems at a $14.35 per-problem cap, exceeding Leanstral 1.5's published 34.

Solving Open Problems

h1 settled eight open problems in Formal Conjectures:

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	$
OEIS A108081	$
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
Written on the Wall II, 100	$\alpha(G) \leq \lceil (\max_v l(v) + \frac{1}{2}\\|\deg G^c\\|_2)/2 \rceil$ for connected $G$
Written on the Wall II, 314	Connected triangle-free $G$ with induced paths of ≤4 vertices is well totally dominated

The system also found misformalizations in Formal Conjectures (e.g., the Poincaré conjecture missing a hypothesis), producing short disproofs of written statements.

The Bitter Lesson for Specialized Workflows

Matched-model comparisons:

Goedel-Architect: h1 with DeepSeek V4 Flash matches its pass@1 at comparable cost, then reaches 598 solves vs. 597 at pass@4 with informal proof seeding, at $1.08 vs.$ 1.47 per problem.
Numina-Lean-Agent: GPT-5.2 alone in h1 solves all twelve Putnam 2025 problems (including A5, which needed Numina's hand-designed subagent workflow), spending $81.52 vs.$ 1,000 budget on A5.
AlphaProof Nexus: On five open Erdős problems, h1's pass@1 reaches 82.5% at $121, exceeding APN basic's pass@3 (75.4% at$ 191) and full APN (76% at $317).

Persisting vs. Repetition

The paper demonstrates that longer attempts can be more efficient than repetition:

pass@1 with extended budget reaches 82.5% at $138 mean spend (including failures)
pass@3 needs $202 to reach at least that rate
The optimal depth-breadth balance depends on budget and is hard to set in advance

Harness Design Matters

Key findings on what makes a harness effective:

Efficient interface: h1 solves 69 Putnam100 problems vs. AxProverBase's 18 with the same Gemini 3 Flash model at $20 budget. AxProverBase's 42.2% of failed compilations stop at invalid library imports, which cannot occur in h1.
Persistence and reflection: Detailed prompts outperform one-line prompts on open problems; reflection raises DeepSeek V4 Flash from 554 to 598 PutnamBench solves.
Context management: Output accounts for 89% of AxProverBase's $17.39 per problem vs. 34% of h1's$ 9.00. h1 reuses 74–94% of input from cache vs. AxProverBase's ≤0.5%.
Turns between reflections: Ten turns between reflections solves 72 Putnam100 problems vs. 50 with one turn, while 200 turns drops to 60 (context rot).
Reasoning effort: Higher reasoning effort with Gemini 3.1 Pro solves 99 Putnam100 problems at $5.34 each vs. 89 at$ 20.63 with low effort.

Theoretical and Practical Implications

Implications for ATP Research

Evaluation standards: The paper argues that cost accounting should become standard practice—attempt counts without inference budgets are misleading when output tokens cost 100× cached input.
The bitter lesson extends to harness design: Simple loops with efficient interfaces can match or outperform complex workflows, suggesting that human effort should go into interfaces rather than prescribed workflows.
Model progress closes gaps: Newer models convert more training compute into capabilities that an unchanged simple loop directly benefits from (e.g., Opus 4.8 in h1 overtaking MerLean with Opus 4.7).

Practical Recommendations

Before designing a workflow, try a frontier model in a simple loop at a realistic budget.
Harnesses should provide: persistent workspace, immediate feedback, retrieval tools, robust failure handling, and context management—while leaving how to prove to the model.
The depth-breadth trade-off (longer attempts vs. repetition) should be left to the model rather than hand-set budgets.

Scaling Considerations

The paper acknowledges limitations: h1 works on a single file, while larger formalizations (e.g., Fermat's Last Theorem, entire textbooks) require dependency management, parallel agents, and codebase-level validation. Following the bitter lesson, these should be added without prescribing their use (e.g., letting agents communicate freely rather than through fixed hierarchies).

Conclusion

The paper's central message: simple test-time scaling with frontier models can match or outperform specialized workflows in automated theorem proving. The authors demonstrate this with h1, a simple harness that reaches state-of-the-art results across benchmarks, settles open problems, and Pareto-dominates specialized systems at matched models and comparable cost.

The key insight is that harness design still matters—but for efficiency of interaction (interface, persistence, context management) rather than for prescribing proof strategies. The bitter lesson applies: human domain knowledge is best spent on building efficient interfaces that let frontier models scale their reasoning, not on encoding proof strategies that models can discover themselves.

Future directions: Scaling simple loops to codebase-level formalizations, parallel agents sharing intermediate results, richer tools (numerical computation, simulation, web search), and ultimately models that build and deploy their own harnesses.