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

> A simple agentic loop with efficient Lean feedback and test-time scaling matches or outperforms specialized theorem-proving workflows, solving eight open problems at lower cost.

- **Source:** [arXiv](https://arxiv.org/abs/2610.35962)
- **Published:** 2026-10-31
- **Permalink:** https://picx.dev/p/A8O3KT
- **Whiteboard:** https://picx.dev/p/A8O3KT/image

## Summary

# 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:

1. **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.
2. **External validator**: Checks the proof against the original statement (via SafeVerify), rejecting placeholders and added assumptions.
3. **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).
4. **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 | $|(A+A)\cap[2N]|/|A\cap[N]| \to \infty$ for thin asymptotic bases |
| 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 |
| 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**:

1. **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.

2. **Persistence and reflection**: Detailed prompts outperform one-line prompts on open problems; reflection raises DeepSeek V4 Flash from 554 to 598 PutnamBench solves.

3. **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%.

4. **Turns between reflections**: Ten turns between reflections solves 72 Putnam100 problems vs. 50 with one turn, while 200 turns drops to 60 (context rot).

5. **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

1. **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.

2. **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*.

3. **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.

---

_Markdown view of https://picx.dev/p/A8O3KT, served by PicX — AI-generated visual whiteboard summaries of research papers._