Researchers at Meta and New York University have built a stripped-down artificial intelligence system for proving mathematical theorems that matched or beat carefully engineered Lean proof workflows — and did so at a lower cost.

The system, called h1, advances a simple argument: in automated theorem proving, simplicity can beat complexity, provided the model receives good feedback.

A Minimal Agentic Loop

The work comes from Meta's FAIR research team and NYU. In a paper titled "h1: A Taste of the Bitter Lesson in Automated Theorem Proving," released on October 25, 2026, the researchers describe h1 as a minimal agentic loop that connects frontier large language models to Lean 4 and feeds them verifier results in real time.

Lean 4 is an open-source proof assistant in which mathematical arguments are written as code, so a compiler rather than a human reviewer checks each step. That setup gives the verifier final say: a proof only counts once it compiles.

Most automated provers wrap the language model in an elaborate scaffold, using predefined workflows that split problems into pieces, route subtasks, and orchestrate many moving parts. The h1 framework skips that machinery and instead relies on a few simple mechanisms:

• Persistent file editing, so the model works on a proof file that keeps its state between steps
• Immediate compiler feedback after every edit, so errors surface right away
• Reflection, using the language model's own ability to reason about what went wrong

According to the paper, h1's performance stems mainly from an efficient interface with Lean, rather than from sophisticated orchestration.

Benchmark Results

The research reports that h1 reached state-of-the-art performance on several formal theorem-proving benchmarks. On PutnamBench, a benchmark built from problems in the William Lowell Putnam Competition — the annual mathematics contest for North American undergraduates — it scored 670 out of 672 using GPT-5.5. On the FATE-X assessment, h1 scored 90 out of 100.

The system also resolved eight open problems in the FormalConjectures collection. These include variants of the Erdős problems, a set of questions named after the prolific mathematician Paul Erdős. Because such problems are stated in Lean's formal language, resolving them means producing machine-checked proofs rather than prose arguments.

The most direct comparison is with DeepMind's AlphaProof Nexus. On Erdős problem resolutions, h1 posted an 82.5% success rate, while AlphaProof Nexus came in at 76%. The cost gap was wider than the accuracy gap: h1 spent $121 per successful proof, compared with $317 for AlphaProof Nexus.

The Bitter Lesson, Applied to Mathematics

The paper's title points to the "bitter lesson" — the term AI researcher Rich Sutton coined in a 2019 essay for the idea that scalable, general-purpose methods powered by heavy computation tend to outperform specialized, handcrafted techniques over time.

This is not Meta's first attempt at the problem. The research builds on earlier Meta work, including the HTPS neural theorem prover introduced in 2022, and reflects a shift in approach. Earlier systems focused on building smarter search around the model, while h1 focuses on letting the model interact directly with the verifier.

Timing matters as well. h1's results depend on frontier models such as GPT-5.5, and the strong PutnamBench score was achieved with that model.

What This Means

The cost figures are the most practical part of the work. A drop from $317 to $121 per successful proof changes which problems are worth trying at all. When each attempt costs less, teams can run more attempts on harder or more speculative conjectures. The machine-checked nature of the results is part of the appeal as well: progress on formal proving draws attention well beyond mathematics, since proof assistants are also used to verify software and hardware designs.

Some caveats apply. Benchmark scores show performance on specific test sets, and PutnamBench is close to saturated at 670 out of 672, so how systems fare on open-problem collections such as FormalConjectures is the measure most worth watching next. The h1 approach also depends heavily on the frontier model underneath it.

The paper's broader message is that a strong base model paired with clean verifier feedback may matter more than elaborate scaffolding — a bet that, on these benchmarks, paid off.

Source: CryptoBriefing