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

h1. A Taste of the Bitter Lesson in Automated Theorem Proving. By Skander Moalla and four others, from FAIR at Meta, EPFL, and two other institutions. Published on the twenty-fifth of October.

Progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models. Formal theorem proving has gone another way, relying more and more on human-designed workflows around those models: planning, decomposition, and orchestrating specialized provers. That raises a bitter-lesson question. Can a simple agentic loop that scales test-time compute match those workflows? The answer reported here is largely yes, provided the loop gives the model an efficient way to work with Lean.

The question matters because formal verification must scale to keep up with frontier models that are producing research mathematics. New workflows rarely settle it, since their gains are often confounded with stronger models or more compute.

The instrument is h1, a simple harness. It gives a model an efficient interface to Lean 4, and keeps it working through verifier feedback and self-reflection, without imposing any decomposition or search structure. What it leaves out is as telling as what it keeps. There is no planner deciding how to break a theorem apart, and no search procedure choosing among branches. What remains is the model, the verifier, and the loop that joins them, with feedback from Lean driving each next attempt.

Even so, h1 reaches state-of-the-art results on PutnamBench, FATE-X and FormalConjectures100-Solved, and settles eight open problems in FormalConjectures. At matched models, it matches or outperforms specialized workflows such as Goedel-Architect and AlphaProof Nexus. Surprisingly, a single attempt, pass at one, can often scale to solve open problems.

The claim carries its own limit. Ablations and matched-model comparisons with Claude Code and AxProverBase show that simplicity alone is not enough. An efficient Lean interface largely determines both cost and solve rate. So the result is not that any bare loop wins. It is that a simple loop with efficient execution feedback holds its own against specialized workflows when the underlying model is held fixed. That condition is deliberate. Because the gains of new workflows are so often confounded with stronger models or more compute, the head-to-head results are reported at matched models, and that is what lets them speak to the question at all.

The recommendation follows directly. Before prescribing a workflow, future work should evaluate frontier models with efficient execution feedback, or risk a bitter lesson of its own. A new workflow, on this view, has to beat a plain loop given the same model and a good interface.