The Bitter Lesson Reaches Automated Theorem Proving

Introduction

Large language models have made progress in informal mathematics by scaling chain-of-thought reasoning, agentic loops, and test-time computation. Formal theorem proving is different: every proposed step must survive a strict checker such as Lean 4. As a result, recent systems have increasingly wrapped models in human-designed workflows involving planning, decomposition, search, and specialized provers.

The paper “h1: A Taste of the Bitter Lesson in Automated Theorem Proving” asks whether those structures are always necessary. If a model is given a good interface to Lean, allowed to inspect verifier errors, and encouraged to reflect and try again, can a simple loop compete with carefully engineered systems?

What h1 changes

h1 is a lightweight harness around Lean 4. It does not require the model to split a theorem into predefined subgoals, follow a fixed search strategy, or coordinate a collection of specialized agents. Instead, the model works directly in the formal environment: it proposes proof code, receives execution feedback, revises the attempt, and continues.

The reported findings include:

• state-of-the-art performance on PutnamBench, FATE-X, and FormalConjectures100-Solved;
• eight previously open problems settled in FormalConjectures;
• performance matching or exceeding specialized workflows such as Goedel-Architect and AlphaProof Nexus when the underlying models are matched;
• evidence that a single attempt, measured as pass@1, can solve open problems in many cases.

The last result is particularly notable. It suggests that success does not always require generating a large collection of candidate proofs and selecting among them. A model that can efficiently use formal feedback may complete the task within one sustained interaction.

Where the bitter lesson appears

The paper uses the “bitter lesson” as a warning against assuming that human-designed structure will always beat scale. Comparisons between theorem-proving systems are often confounded: one workflow may use a stronger model, more calls, or a larger test-time budget. Under matched conditions, h1 provides evidence that a relatively generic agent loop can capture much of the benefit attributed to more elaborate orchestration.

That does not mean simplicity is sufficient. Ablations and comparisons with Claude Code and AxProverBase indicate that the Lean interface is a major determinant of both cost and solve rate. Feedback must arrive efficiently and be usable by the model. A theoretically simple loop can still be expensive or ineffective if every verification cycle is slow, noisy, or difficult to interpret.

Why it matters

For formal mathematics, the practical lesson is methodological as much as architectural. Before adding planners, decomposers, or specialized provers, researchers should establish a strong baseline with efficient execution feedback. Evaluations should also match model capability and test-time computation so that workflow gains are not confused with extra resources.

h1 does not show that every theorem is best handled by a single loop, nor does it eliminate the value of search or decomposition. Its contribution is a demanding baseline: additional structure should demonstrate benefits that justify its extra complexity and cost. As frontier models produce more mathematical conjectures, reducing the friction between language models and formal verifiers may be as important as inventing another layer of orchestration.

Source: Hugging Face Daily Papers