Meta and NYU paper shows h1 loop beats hand-built Lean workflows
The result suggests Lean theorem proving needs less orchestration than commonly assumed, provided the model gets fast compiler feedback and enough retries. Teams building formal-math or proof-verification systems can save engineering effort by testing a simple feedback loop before designing custom pipelines. The cost figure of US$1.08 per PutnamBench problem also gives a concrete budget baseline against heavier agentic setups.
A paper from Meta and NYU introduces h1, a minimal loop that gives a model fast Lean compiler feedback and search tools, with no hand-designed planning beyond a progress summary before each round. On PutnamBench with the same underlying model, h1 solved 598 of the problems versus 597 for the hand-built Goedel-Architect workflow, at US$1.08 versus US$1.47 per problem. The interface still matters: with Opus 4.8, h1 solved 83 of 100 hard algebra problems against 63 for Claude Code. The authors argue that much of the reported gain from elaborate theorem-proving workflows may come from more compute or stronger models rather than the workflow itself.
New Meta, NYU paper shows that a simple loop with good Lean tools and more compute matches or beats hand-built theorem-proving workflows.
Systems that write math proofs in Lean, a language a computer can check, increasingly use hand-designed workflows that plan and split up problems. Their gains often come with stronger models or more compute, hiding what the workflow adds.
They built h1, a loop that gives the model fast Lean feedback and search tools, and keeps it working after each failed check. It imposes no plan, only a progress summary before each new round.
With the same model, h1 beat the hand-built Goedel-Architect on PutnamBench, 598 problems to 597, at $1.08 against $1.47 per problem. The interface still matters: with Opus 4.8, h1 solved 83 of 100 hard algebra problems, against 63 for Claude Code.
