Researchers at FAIR at Meta have posted h1, a paper that asks a direct question about AI theorem proving: do you need a complex, hand-built workflow around a language model, or will a plain loop with good tools and more compute do the same job? Their answer, for formal proofs in the Lean language, is mostly the plain loop. The paper was submitted to arXiv on October 25, 2026. Its authors are Skander Moalla, Ahmad Rammal, Niket Patel, Rémi Munos and Julia Kempe, with co-affiliations at EPFL, ENPC and New York University.
The headline results: h1 with GPT-5.6 Sol settled eight problems that the Formal Conjectures collection listed as open, and with GPT-5.5 it solved 670 of the 672 problems in PutnamBench in a single run per problem. The more useful finding for engineers is about agent design, not math.
The question: workflows or a simple loop
Lean is a proof assistant. A statement and its proof are written as code, and the compiler checks every step. That makes it a natural place for AI agents, because a machine can check exactly whether a proof proves the stated theorem. OpenAI used the same kind of check when it published Lean certificates for the ten math results it credited to Astra.
Many recent provers wrap a frontier model in a fixed structure: plan the proof, split it into lemmas, hand parts to separate agents or specialized provers, then review. The authors frame this as a "bitter lesson" question, after Rich Sutton's essay arguing that general methods that scale with compute tend to beat methods built on human domain knowledge. If frontier models already reason and use tools well, does the hand-designed structure still pay for itself?
How h1 works
h1 imposes no plan, decomposition or search order. In each iteration the model edits one persistent Lean file over many turns. Every edit compiles and returns errors and open goals. The model can search the Mathlib library (with LeanExplore, Loogle and grep), test proof fragments in the Lean REPL, and ask the language server for goals and definitions. It decides which tools to use.
When the model submits, an external validator (SafeVerify) checks the proof against the original statement and rejects placeholders or added assumptions. If the proof fails, a separate reflection call compacts the transcript into verified progress, lessons from failed attempts and useful lemma names, and the next iteration starts from the current file with that summary. The loop runs until the validator accepts a proof or a cost cap stops it. The authors compare each extra iteration to appending "Wait" to a model's reasoning in the earlier s1 paper.
The paper reports a cost for each of its own runs, computed from recorded token usage and published API prices. That matters because, as the authors point out, one "attempt" can mean very different amounts of compute in different systems.
Results
On benchmarks, the authors report these results for h1 with GPT-5.6 Sol, each from a single run per problem:
- FATE-X (100 algebra problems at PhD qualifying-exam level or beyond): 90 solved, at $38 per problem.
- FC100-solved (100 Formal Conjectures problems with known informal solutions): 78 solved.
- FormalQualBench (23 theorems at PhD qualifying-exam level): 14 solved.
- IMO 2026, as formalized by Axiom: all six problems.
A cheaper open-weight model also does well in the same loop. DeepSeek V4 Flash in h1 solved 43 FATE-X problems at a $14.35 per-problem cap, above the 34 published for Leanstral 1.5. On FC100-solved it reached 64 at $4.89 per problem.
On open problems, the team ran h1 on 236 targets marked open in Formal Conjectures. It settled eight: variants of Erdős problems 138 and 337, three OEIS conjectures (A108081, A211417 and A022030), the existence of an AME(9,10) state (Open Quantum Problem 35), and two conjectures from Written on the Wall II, which were proved after the team corrected their formal statements. The authors' pull request to Formal Conjectures, merged on September 24, 2026, marks five of the eight solved: the Erdős 138 and 337 variants, A108081, A211417 and Open Quantum Problem 35. It also cites independent concurrent work on the Erdős 138 variant and an earlier proof sketch for the A211417 congruence. The system also found misformalizations, formal statements that do not say what the conjecture means. One example was the Poincaré conjecture entry, which was missing a hypothesis, so h1 produced a short disproof of the statement as written. The same question, whether a machine check proves what mathematicians meant, came up in reactions to Axiom's Lean proof of the finite simple groups classification.
Head to head with specialized systems
The core comparisons hold the model fixed and change only the harness:
- PutnamBench, DeepSeek V4 Flash: h1 reached 598 solves at an estimated $1.08 per problem. Goedel-Architect reached 597 at best of four runs seeded with natural-language proofs, at $1.47.
- Five open Erdős problems, Gemini 3.1 Pro: one h1 attempt reached 82.5% at $121 mean cost per success. Full AlphaProof Nexus reached 76% at $317, and its basic agent reached 75.4% at $191 with three attempts.
- Putnam 2025: GPT-5.2 alone in h1 solved all 12 problems for $565 in total, including problem A5, for which Numina-Lean-Agent used a separate multi-agent workflow and a $1,000 budget.
The authors say that across 707 benchmark problems compared against specialized workflows, they found two exceptions. Full AlphaProof Nexus solved Erdős 125, where all 16 h1 attempts ended in Lean timeouts. MerLean with Opus 4.7 proved BurnsidePrimeDegree, which h1 with Opus 4.8 did not prove in their run, though h1 with GPT-5.6 Sol did.
What a simple harness still needs
The paper does not say design is irrelevant. With the same model, simple loops differed several-fold in solve rate and cost. Some measured examples:
- Small edits beat rewrites. With Gemini 3 Flash and a $20 budget, AxProverBase, which regenerates the whole proof after each round, solved 18 of 100 Putnam problems against 69 for h1.
- Persistence beats a stopping model. With Opus 4.8 on FATE-X, native Claude Code solved 63. Adding h1's prompt and Lean tools through MCP raised that to 73, and h1 reached 83.
- A moderate number of turns between reflections works best. With Gemini 3 Flash on Putnam100 and Gemini 3.1 Pro on FATE-X, ten turns solved 72 and 65 problems; one turn solved 50 and 39; 200 turns solved 60 and 52.
- Higher reasoning effort was cheaper. With Gemini 3.1 Pro on Putnam100, low effort solved 89 problems at $20.63 each and high effort solved 99 at $5.34 each.
Why it matters
The authors expect these lessons to transfer to other agents that work against a verifier, such as software verification and coding in large codebases. Their advice: before you design a workflow, try a frontier model in a simple loop with an efficient interface and a realistic budget. In formal math, they write, spending compute on the model's reasoning and human effort on the interface works best for now.
The limits are clear in the paper. h1 works on a single file, so very large formalizations that span many files are out of scope. Axiom's agent-built Lean proof of the classification of finite simple groups, which Axiom says runs to about 43.1 million lines, is that kind of project. Its tools cover only Lean, not computation or web search. The authors also note they cannot fully rule out benchmark exposure in training, though they used models released before Putnam 2025 and IMO 2026 where possible. The paper does not link a code repository; it describes the harness, prompts and reflection protocol in its appendices.
