Meta FAIR h1 solves 670/672 Putnam, beats AlphaProof Nexus

h1, a bare-bones agentic harness from a team at FAIR at Meta and partner universities, solves 670 of 672 problems on PutnamBench with GPT-5.5 and settles eight open problems in FormalConjectures, according to a new arXiv paper. The authors pose it as a test of the bitter lesson in a domain where human-designed workflows — planning, decomposition, orchestrating specialized provers — have been the default.

The system does not plan or search. The paper describes it as "a simple harness that gives a model an efficient interface to Lean 4 and keeps it working through verifier feedback and self-reflection, without imposing a decomposition or search structure." On FATE-X, h1 scored 90 of 100 using GPT-5.6 Sol. On FormalConjectures100-Solved it reached 78 of 100.

The head-to-head with AlphaProof Nexus is where the cost argument lands. On five open Erdős problems, h1 reached 82.5% success at $121 mean cost per solved problem, against full AlphaProof Nexus at 76% and $317. The eight settled open problems the paper lists include variants of Erdős 138 and 337, three OEIS conjectures (A108081, A211417, A022030), the existence of an AME(9,10) state, and two conjectures of Written on the Wall II.

Ablations against Claude Code and AxProverBase push against a lazy reading of the result. The paper reports that in AxProverBase, "output accounts for 89% of its $17.39 per problem, against 34% of h1's $9.00" — the Lean interface, not the loop, moves cost. The authors recommend that "future work evaluate frontier models with efficient execution feedback before prescribing workflows, at the risk of bitter lessons."