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

Advances in automated theorem proving (ATP) have largely been driven by systems built on large language models (LLMs). Formal proof systems often wrap an LLM in a complex harness with pre-designed planning, retrieval, and multi-agent orchestration. However, it is unclear whether benchmark advances come from these inductive biases, test-time scaling, or more capable models. We build `h1`, a simple harness of generic components that allows for unbounded test-time scaling for theorem proving in the Lean proof assistant, and study how far it can go with only Lean tools, verifier feedback, and self-reflection sustaining progress. `h1` achieves state-of-the-art results and advances the cost–accuracy frontier on PutnamBench, FATE-X, and FormalConjectures100-Solved, and resolves 9 open problems in FormalConjectures. It matches or outperforms more specialized systems, including AlphaProof, Goedel-Architect, Numina-Lean-Agent, OpenGauss, Aleph, and simpler alternatives like Humanfia, AxProverBase, and Claude Code, at matched models where available. On open Erdős problems, scaling `h1`'s pass@1 can be more cost-effective than repetition within `h1` or AlphaProof Nexus (APN) basic, and surpass the full APN system. Our ablations show how tool use, prompting, self-reflection, thinking budget, and turns per iteration shape scaling efficiency.