Meta and NYU’s h1 system beats elaborate theorem-proving workflows at lower cost

The h1 system, developed by researchers from Meta's FAIR team and NYU, represents a breakthrough in automated theorem proving. By using a minimal agentic loop that connects frontier large language models to Lean 4 with real-time verifier feedback, h1 has matched or exceeded the performance of more complex systems while dramatically reducing costs.

Unlike traditional automated provers that rely on elaborate scaffolding and predefined workflows, h1 employs just a few simple mechanisms: persistent file editing to maintain state between steps, immediate compiler feedback to surface errors quickly, and reflection using the language model's own reasoning capabilities.

Benchmark Results

The system has demonstrated impressive performance on formal theorem-proving benchmarks. On PutnamBench, h1 scored 670 out of 672 using GPT-5.5, while on the FATE-X assessment it achieved 90 out of 100. Most notably, h1 resolved eight open problems in the FormalConjectures collection, including variants of Erdős problems.

When directly compared to DeepMind's AlphaProof Nexus, h1 showed superior performance with an 82.5% success rate on Erdős problem resolutions, compared to AlphaProof Nexus's 76%. The cost advantage was even more substantial, with h1 spending $121 per successful proof versus $317 for AlphaProof Nexus.

The Bitter Lesson Applied

The research reflects the 'bitter lesson' concept - that scalable, general-purpose methods tend to outperform specialized, handcrafted techniques over time. This approach represents a shift from Meta's earlier theorem-proving efforts like HTPS neural theorem prover, which focused on building smarter search around the model.

The significant cost reduction makes previously impractical problems more accessible. When each attempt costs less, teams can run more attempts on harder or more speculative conjectures, potentially accelerating mathematical discovery. However, the approach depends heavily on frontier models like GPT-5.5, and benchmark performance may vary on different problem sets.