# Meta and NYU paper finds simple Lean loop matches hand-built theorem-proving workflows

> Original title: New Meta, NYU paper shows that a simple loop with good Lean tools and more compute matches or beats hand-built theorem-proving workflows.

- Source: Rohan Paul
- Published: 2026-11-01T19:25:28.000Z
- Bad Influence: https://badinfluence.news/items/vu8wdgj538u93xg6q76ghzyb4
- Original: https://x.com/rohanpaul_ai/status/2116974925655519727

## Summary

Meta and NYU researchers present h1, a loop that gives a model fast Lean feedback and search tools without imposing a fixed plan. With the same model, h1 solved 598 of 672 PutnamBench problems against 597 for the hand-built Goedel-Architect, at $1.08 per problem against $1.47. The paper also reports that with Opus 4.8, h1 solved 83 of 100 hard algebra problems, versus 63 for Claude Code.

## Post

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.

![](https://badinfluence.news/api/img-proxy?u=https%3A%2F%2Fpbs.twimg.com%2Fmedia%2FHWEBSW3a4AAsaZu.jpg&mode=thumb&exp=1793836800&sig=a62f09bb4b533032)