h1 is a research harness that lets a language model develop proofs in Lean 4, a programming environment whose checker can verify formal proofs. The authors report strong results on several specific benchmarks, but each score belongs to its own model and test set. Their headline cost comparison with AlphaProof Nexus covers five Erdős problems and counts costs only among successful runs. The authors’ paper describes the system and its experiments.
How h1 works with Lean 4
h1 gives a model a persistent Lean file to edit over multiple turns. After each edit, Lean returns compiler errors and any proof goals that remain open. The model can search Mathlib, Lean’s mathematics library, check small fragments in a Lean REPL, and use language-server information. The harness does not prescribe a proof plan or search tree; the model chooses how to use those tools.
If a submitted proof is rejected, a reflection model condenses the work so far and the verifier’s feedback for another attempt. The process continues until validation succeeds or the inference budget runs out.
That final check involves more than compilation. SafeVerify compares the submission with the original challenge, checks the required declarations and permitted axioms, then replays accepted declarations through Lean’s kernel. A file that compiles could still contain unfinished proof goals or rely on changed assumptions or extra axioms, so compilation alone is not the final test.
What the benchmark scores cover
The authors report 670 of 672 PutnamBench problems solved with GPT-5.5, using one run per problem without repeats or parallel attempts. With GPT-5.6 Sol, they report 90 of 100 FATE-X problems, 78 of 100 FC100-solved problems, 14 of 23 FormalQualBench theorems, and all six IMO 2026 problems. FATE-X consists of algebra problems at PhD qualifying-exam level or beyond. These are separate benchmarks, not a single score for mathematical ability. (Study details)
The paper also reports eight targets solved from 236 Formal Conjectures targets treated as open in its evaluation: variants of Erdős 138 and 337; OEIS A108081, A211417, and A022030; Open Quantum Problem 35; and Written on the Wall II Conjectures 100 and 314. The authors say the last two were proved after errors in their formalized statements were corrected.
What the AlphaProof Nexus comparison counts
The highlighted cost-success comparison uses Gemini 3.1 Pro on five Erdős problems for which all three evaluated systems had at least one success. On that subset, h1 reached 82.5% pass@1, meaning its success rate with one attempt; full AlphaProof Nexus reached 76%. The reported mean costs below are conditional on success.
| System | Pass@1 on five problems | Mean cost per successful proof, conditional on success |
| h1 | 82.5% | $121 |
| Full AlphaProof Nexus | 76% | $317 |
The $317 AlphaProof Nexus figure excludes inference costs for its AlphaProof component. The five-problem comparison also leaves out Erdős 125, where all 16 h1 replicas ended in Lean REPL timeouts. Counting failed groups as well, the paper reports a $138 mean spend for h1 at pass@1 on the five-problem set; reaching at least 82.5% with pass@3 required $202.
Across all six Erdős problems, the reported pass@1 rates were 68.75% for h1 and 71.67% for full AlphaProof Nexus; h1’s pass@3 rate was 79.73%. These are experimental API-equivalent token-cost estimates, calculated from recorded token use and reference API rates, not product prices or necessarily actual spending. (The paper’s comparison and cost method)
What a formally checked proof establishes
Lean and SafeVerify can establish that a proof follows from the formal statement and assumptions submitted for checking. They do not, by themselves, establish that the formal statement faithfully captures the intended informal conjecture. The corrections to Written on the Wall II Conjectures 100 and 314 show why those are separate questions: the authors report proofs of the corrected formal statements.
