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

A 30 October 2026 arXiv paper by Skander Moalla and co-authors reports that h1, a simple agentic loop giving a language model an efficient interface to Lean 4 with verifier feedback and self-reflection, reaches state-of-the-art results on PutnamBench, FATE-X and FormalConjectures100-Solved and settles eight open problems in FormalConjectures. At matched models, h1 matches or outperforms specialized workflows such as Goedel-Architect and AlphaProof Nexus, with ablations against Claude Code and AxProverBase showing that an efficient Lean interface largely determines cost and solve rate. The authors recommend that future work evaluate frontier models with efficient execution feedback before prescribing human-designed workflows of planning, decomposition and prover orchestration.

Computer Science Machine Learning Submitted on 25 Oct 2026 v1 https://arxiv.org/abs/2610.35962v1 , last revised 30 Oct 2026 this version, v2 Title:h1: A Taste of the Bitter Lesson in Automated Theorem Proving View PDF https://arxiv.org/pdf/2610.35962 HTML experimental https://arxiv.org/html/2610.35962v2 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. Submission history From: Skander Moalla view email https://arxiv.org/show-email/956eee7f/2610.35962 Sun, 25 Oct 2026 11:07:24 UTC 1,044 KB \ v1\ https://arxiv.org/abs/2610.35962v1 v2 Fri, 30 Oct 2026 17:36:57 UTC 1,066 KB Additional Features References & Citations Loading... Bibliographic and Citation Tools Bibliographic Explorer What is the Explorer? https://info.arxiv.org/labs/showcase.html arxiv-bibliographic-explorer Connected Papers What is Connected Papers? https://www.connectedpapers.com/about Litmaps What is Litmaps? https://www.litmaps.co/ scite Smart Citations What are Smart Citations? https://www.scite.ai/ Code, Data and Media Associated with this Article alphaXiv What is alphaXiv? https://alphaxiv.org/ CatalyzeX Code Finder for Papers What is CatalyzeX? https://www.catalyzex.com DagsHub What is DagsHub? https://dagshub.com/ Gotit.pub What is GotitPub? http://gotit.pub/faq Hugging Face What is Huggingface? https://huggingface.co/huggingface ScienceCast What is ScienceCast? https://sciencecast.org/welcome Demos Recommenders and Search Tools Influence Flower What are Influence Flowers? https://influencemap.cmlab.dev/ CORE Recommender What is CORE? https://core.ac.uk/services/recommender IArxiv Recommender What is IArxiv? https://iarxiv.org/about arXivLabs: experimental projects with community collaborators arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website. Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them. Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs https://info.arxiv.org/labs/index.html .