Meta and NYU's h1 matches or beats elaborate Lean workflows at lower cost, paper says
In brief
- Meta FAIR and NYU released the h1 paper on October 25, 2026.
- h1 connects frontier LLMs to Lean 4, feeding them verifier results in real time.
- h1 scored 670 of 672 on PutnamBench with GPT-5.5 and 90 of 100 on FATE-X, the paper reports.
- h1 spent $121 per successful proof versus $317 for AlphaProof Nexus, by the paper's numbers.
- Caveats: PutnamBench is near saturation, and h1 relies heavily on the underlying model.
A minimal loop instead of a scaffold
Most automated provers wrap the language model in an elaborate scaffold with predefined workflows. h1 skips all that. The researchers describe it as a minimal agentic loop that connects frontier large language models to Lean 4 and feeds them verifier results in real time.
That's the whole pitch.
The paper argues h1's performance comes mainly from an efficient interface with Lean, not from orchestration. Earlier systems (including Meta's own HTPS neural theorem prover, introduced in 2022) focused on building smarter search around the model, while h1 lets the model interact directly with the verifier. The "bitter lesson" in the title is the idea that scalable, general-purpose methods powered by heavy computation tend to outperform specialized, handcrafted techniques over time.
Benchmarks and cost per proof
According to the paper, as reported by Crypto Briefing, h1 reached state-of-the-art performance on several formal theorem-proving benchmarks. It scored 670 out of 672 on PutnamBench using GPT-5.5. It scored 90 out of 100 on the FATE-X assessment.
The researchers also say h1 resolved eight open problems in the FormalConjectures collection, including variants of Erdős problems. That's their claim.
On Erdős problem resolutions, the paper puts h1's success rate at 82.5%, against 76% for DeepMind's AlphaProof Nexus. The cost numbers are where the gap gets wide. By the paper's own comparison, h1 spent $121 per successful proof while AlphaProof Nexus spent $317 (a figure from the h1 paper, not from DeepMind).
The cost gap is wider than the accuracy gap.
The caveats
Don't read too much into the headline scores. Benchmark scores show performance on specific test sets, and PutnamBench is close to saturated at 670 out of 672, so there isn't much room left on that test to separate systems.
h1 also depends heavily on the underlying frontier model. Its PutnamBench result was achieved with GPT-5.5, and the report says h1's results depend on frontier models like it.
So the scaffold got thinner, but the reliance on a frontier model didn't go away.
Frequently asked questions
How does Meta and NYU's h1 theorem prover work?
The researchers describe h1 as a minimal agentic loop. It connects frontier large language models to Lean 4 and feeds them verifier results in real time, instead of wrapping the model in elaborate scaffolds with predefined workflows. The paper argues its performance comes mainly from that efficient interface with Lean.
What does the 'bitter lesson' in the h1 paper's title mean?
It refers to the idea that scalable, general-purpose methods powered by heavy computation tend to outperform specialized, handcrafted techniques over time. h1 applies that idea by letting the model interact directly with the Lean verifier rather than building smarter search around it.
How does h1's cost compare with DeepMind's AlphaProof Nexus?
According to the h1 paper, h1 spent $121 per successful proof, compared with $317 for AlphaProof Nexus. On Erdős problem resolutions, the paper reports an 82.5% success rate for h1 versus 76% for AlphaProof Nexus. These are the paper's figures, not DeepMind's.
