h1: A Taste of the Bitter Lesson in Automated Theorem Proving
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.
The following analysis is generated by AI and may contain errors. It is separate from the authors’ abstract and is not peer review.
Research summary
The paper demonstrates that a simple agentic loop with an efficient Lean interface and test-time scaling can match or outperform complex, human-designed workflows in automated theorem proving, settling open mathematical problems and achieving state-of-the-art results on major benchmarks. This work provides a compelling empirical case for the "bitter lesson" in the context of agent harness design, suggesting that future progress will come from scaling model capabilities and interaction efficiency rather than from increasingly elaborate orchestration strategies.
Methodology
The paper proposes "h1," a minimalist agentic harness for Lean 4 theorem proving that relies on a simple ReAct-style loop with an efficient interface to the Lean compiler, library search tools, and a reflection mechanism to compact context. The core methodological contribution is not a new model architecture or training algorithm, but a rigorous empirical demonstration that "bitter lesson" principles apply to harness design: that scaling test-time compute in a simple loop with good tooling outperforms complex, human-designed workflows (like planning, decomposition, or multi-agent orchestration) when using the same frontier models. The methodology is sound, focusing on isolating the variable of harness complexity while controlling for model capability and inference cost.
Results & evaluation
The experimental evaluation is extensive and high-quality. It covers a wide range of benchmarks including PutnamBench, FATE-X, FormalConjectures, and IMO 2026. The paper provides matched-model comparisons against state-of-the-art specialized systems (Goedel-Architect, AlphaProof Nexus, MerLean, etc.), which is crucial for a fair assessment. The results show that h1 achieves state-of-the-art performance, solving open problems and matching or exceeding specialized workflows at lower cost. The analysis of cost-efficiency curves (pass@1 vs pass@k) is particularly insightful, showing that longer single attempts can be more efficient than multiple shorter ones.
Reproducibility
The paper provides detailed appendices on tools, prompts, error handling, and cost accounting. It specifies the exact versions of Lean and Mathlib used, and provides a link to the pull request documenting the newly solved conjectures. While the specific code for the h1 harness is not explicitly linked in the provided text (only the conjectures PR), the level of detail in the prompts and tool descriptions suggests high reproducibility for researchers with access to the same frontier models.
Limitations
The primary limitation is the reliance on proprietary frontier models (GPT-5.6, Opus 4.8, etc.), which are black boxes and subject to rapid change, making long-term reproducibility difficult. The paper also acknowledges that it does not address the challenge of formalizing proofs that exceed the context window or require parallel agents for very large projects, though it suggests this is a natural next step. The cost analysis relies on API pricing, which may not reflect the true compute cost for self-hosted models.
Broader impact
This paper has significant broader impact by challenging the prevailing trend in automated theorem proving towards increasingly complex, human-designed workflows. It provides strong evidence that as LLMs improve, the focus should shift to building efficient interfaces and allowing models to scale their own reasoning, rather than imposing rigid structures. This insight is likely to influence the design of agents in other structured domains, such as software verification and formal methods. The paper demonstrates that a simple agentic loop with an efficient Lean interface and test-time scaling can match or outperform complex, human-designed workflows in automated theorem proving, settling open mathematical problems and achieving state-of-the-art results on major benchmarks. This work provides a compelling empirical case for the "bitter lesson" in the context of agent harness design, suggesting that future progress will come from scaling model capabilities and interaction efficiency rather than from increasingly elaborate orchestration strategies.
Author of this paper? Send a correction.