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

AI summary

Overview

Research area: Machine learning / automated theorem proving, specifically the design of LLM "harnesses" (the tools, context and control loop wrapped around a model) for formal proof in Lean 4.

Technical level: Intermediate. The core argument is conceptual and readable without a proof-assistant background, but the evaluation assumes familiarity with LLM agents, pass@k metrics and inference-cost accounting.

Scope: The paper asks whether a deliberately simple agentic loop with an efficient Lean interface can match human-designed proving workflows at matched models and comparable inference cost.

What This Paper Is About

Recent formal theorem provers wrap frontier language models in elaborate human-designed workflows — planning, lemma decomposition, blueprint search, orchestrating specialized sub-provers. The authors ask a "bitter lesson" question: if models already scale with test-time compute, can a simple loop that only supplies Lean feedback and keeps the model working match those workflows? They answer with h1, a minimal harness, and argue that the value lies not in prescribing a workflow but in providing an efficient, reliable interface to the verifier.

Key Contributions

1. A minimal harness (h1). The model iterates between a multi-turn ReAct block of reasoning and tool calls that edit a persistent Lean file, a submission to an external validator (SafeVerify), and a reflection step that compacts the transcript into a fresh context for the next iteration. No decomposition, planning or search structure is imposed.
2. A matched-model, cost-aware comparison against specialized workflows. The paper compares h1 with Goedel-Architect, MerLean, full AlphaProof Nexus (APN), OpenGauss, Numina, plus simple loops (APN basic, AxProverBase, Claude Code, Humanfia), holding the model fixed where possible and plotting cost–success curves rather than single pass@k points.
3. Evidence that one long attempt can beat repetition. On five open Erdős problems, extending a single h1 attempt (pass@1) Pareto-dominates APN basic at pass@3 and full APN, at lower mean cost per success.
4. Ablations identifying what a simple harness must still get right. Tool access, detailed prompts, reflection, turns between reflections, cache reuse and reasoning effort are each varied to show that interface efficiency, persistence and context management drive both cost and solve rate.

Main Findings

• State-of-the-art results with a single run per problem: with GPT-5.6 Sol, h1 reports 90/100 on FATE-X, 78/100 on FC100-solved, 14/23 on FormalQualBench and all six IMO 2026 problems; with GPT-5.5 it solves 670 of 672 PutnamBench problems. All without repetition or parallelism.
• Extreme persistence is possible: individual accepted attempts reached up to 1,123 rounds of reflection (compaction), 95 active hours, or 7,124 lines of proof.
• Cheap open-weight models beat specialized provers: DeepSeek V4 Flash in h1 solves 43 FATE-X problems at a $14.35 per-problem cap, above Leanstral 1.5's published 34; on FC100-solved it matches AlphaProof's 50 solves below an estimated $0.30 cap and reaches 64 at $4.89, close to the DeepMind (DM) prover agent's 66.
• Beating a stronger baseline's budget: Gemini 3.1 Pro in h1 matches the DM prover agent's 66 FC100-solved solves at a $25 rather than $100 cap, then reaches 73 at $150; GPT-5.6 Sol matches those 66 solves below a $9 cap and reaches 90 FATE-X solves at $38 per problem versus 81 at $113.
• Eight open problems settled: variants of Erdős 138 and 337, OEIS conjectures A108081, A211417 and A022030, the existence of an AME(9,10) state (Open Quantum Problem 35), and two Written on the Wall II conjectures (100 and 314), out of 236 targets selected as open from Formal Conjectures.
• Misformalizations exposed: h1 produced short disproofs of wrongly stated formalizations, for example a Poincaré conjecture statement missing a hypothesis; most have since been fixed upstream.
• Pareto-dominating Goedel-Architect: with the same DeepSeek V4 Flash model, h1 reaches 598 PutnamBench solves versus Goedel-Architect's 597 at pass@4 with informal proof seeding, at an estimated $1.08 versus $1.47 per problem. Goedel-Architect's tool-integrated reasoning baseline reaches only 54.5% at pass@32 on a 200-problem subset, against h1's 89.0% at pass@1 on the full benchmark with the same model.
• No hand-designed workflow needed for the hardest Putnam 2025 problem: GPT-5.2 alone in h1 solves all twelve Putnam 2025 problems, including A5, spending $81.52 on A5 against Numina's $1,000 budget for that problem; total cost $565 versus Numina's $1,800 cap.
• Repetition closes most remaining gaps: on PutnamBench, extra attempts on the last two problems let h1 with GPT-5.5 match Aleph Prover's 672/672 at an estimated $17.86 versus about $74 per problem; on FormalQualBench the best of four h1 runs with Opus 4.6 matches OpenGauss's eight solves under the same four-hour limit.
• Longer attempts beat repetition on open problems: on the five Erdős problems solved by all three systems, h1's pass@1 exceeds APN basic's pass@3 (75.4% at $191) and full APN (76% at $317), reaching 82.5% at $121; with failures charged, pass@1 reaches 82.5% at $138 while pass@3 needs $202.
• One genuine exception: full APN solves Erdős 125, where all sixteen h1 attempts end in Lean timeouts; across the 707 benchmark problems compared, the paper reports only two exceptions where a specialized harness solved something h1 did not.
• Interface efficiency dominates cost: with the same Gemini 3 Flash and a $20 budget, AxProverBase solves 18 Putnam100 problems against h1's 69; 42.2% of AxProverBase's failed compilations stop at an invalid library import, which cannot occur in h1 because its file already imports all of Mathlib.
• Tools matter as a class, not individually: without search tools, the REPL or the language server, h1 solves 49 Putnam100 and 49 FATE-X problems, against 69 and 63 with all tools; removing any single tool from the full set costs at most four solves.
• The loop decides when to stop: native Claude Code with Opus 4.8 solves 63 FATE-X problems, 73 with h1's prompt and Lean tools via MCP, and h1 reaches 83 (81, 95 and 99 on Putnam100).
• Prompts matter most on open problems: on six Erdős problems at a $150 cap, one attempt with detailed prompts outperforms six attempts with one-line prompts; reflection raises DeepSeek V4 Flash from 554 to 598 PutnamBench solves.
• Context reuse versus context rot: AxProverBase spends 89% of its $17.39 per problem on output against 34% of h1's $9.00, and reuses at most 0.5% of input from cache against 74–94% for h1; but with 200 turns between reflections the cached share rises to 86% while solves fall to 60 Putnam100 and 52 FATE-X, versus 72 and 65 at ten turns.
• Thinking harder beats retrying: with Gemini 3.1 Pro, high reasoning effort solves 99 Putnam100 problems at $5.34 each versus 89 at $20.63 with low effort.

Methodology in Plain English

The authors build a harness that does as little as possible beyond connecting a model to Lean 4 well. The model works on one persistent source file, and every edit is compiled immediately so errors and open goals come back as feedback. It can search Mathlib (via LeanExplore, Loogle and grep), run proof fragments in the Lean REPL, and inspect goals and definitions through the language server. When it submits, an external validator checks the proof against the original statement, rejecting placeholders and added assumptions. If rejected, a separate reflection model summarizes what was verified, what failed and which lemmas look useful, then the model continues from where it left off — so more budget means more continued work rather than a restart.

To test whether this is enough, they evaluate on benchmarks of increasing difficulty, from PutnamBench (672 problems) through FATE-X, FormalQualBench, FC100-solved, recent Putnam 2025 and IMO 2026 sets, up to open Formal Conjectures targets. Crucially, they compare systems at the same model and plot solve rate against inference cost per problem, counting failed attempts and capping each problem's cost at the budget. They then run ablations that vary one harness component at a time — tools, prompts, reflection, turns between reflections, reasoning effort — to isolate what drives success.

Why This Matters

Impact on research: The paper argues that many reported gains from specialized proving workflows are confounded with stronger models or larger compute budgets, since one "attempt" can mean up to 16 plan revisions in Goedel-Architect or 50 agent iterations in AxProverBase while both are called pass@1. It recommends treating cost-matched simple loops as the baseline before prescribing a workflow, and it gives a concrete recipe for what a minimal harness must provide: an efficient interface, reliable feedback, persistence and cache-aware context management.

Real-world applications:

• Verification of AI-generated mathematics: as frontier models produce research-level mathematics, mechanically checked proofs become a bottleneck; the paper positions scalable ATP as a necessary component of automated discovery.
• Software verification and coding in large libraries: the authors state their lessons should transfer to agents working against a verifier in rich environments with structured development and retrieval.
• Cost-effective deployment: an open-weight model (DeepSeek V4 Flash) outperforming specialized provers at a $14.35 per-problem cap shows that harness efficiency, not just model choice, controls the bill.
• Benchmark and formalization hygiene: h1 found misformalized statements (including a Poincaré conjecture missing a hypothesis), suggesting automated disproof attempts are a practical audit tool for formalization projects.

Industry relevance: The main lever identified is engineering, not model training — caching, small-step edits, immediate compiler feedback and transient-failure handling. That is directly actionable for teams building long-horizon agents, and it argues against hard-coding orchestration that a next-generation model may simply internalize.

Future Directions

1. Scaling beyond a single file. Formalizations exceeding a context window — Fermat's Last Theorem, entire textbooks, or OpenAI's Navier–Stokes effort with about 10,000 agents exchanging millions of messages over 88 hours — need dependency management across files, codebase-level validation and parallel agents sharing intermediate results.
2. Richer tools without prescribing their use. The current tools cover only Lean, not numerical computation, simulation, visualization or web search; the open question is how to add them while leaving the choice to the model, for example letting agents communicate freely rather than through a fixed hierarchy.
3. Models that build their own harnesses. The authors speculate that a model could eventually construct and deploy its own interface for a problem and outperform human-designed ones.
4. Better evaluation norms. Reporting solve rates without matched inference cost should give way to cost–success curves, and the depth-versus-breadth choice (one long attempt versus many short ones) is budget- and problem-dependent and hard to fix in advance.

Target Audience

Researchers and engineers working on LLM agents, automated theorem proving and formal verification; practitioners building long-horizon agents against a verifier (coding, software verification); and benchmark designers who need to interpret pass@k claims and inference-cost comparisons. Readers evaluating "agentic workflow" papers will find the matched-model, cost-aware methodology the most transferable part.

Authors’ 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.