ReuF2F Benchmark: Best Coding Agent Solves Only 109 of 244 Lean-Formalized Open Math Problems
wellecks · x · 2026-10-21
- Researchers released ReuF2F on arXiv: a Lean 4 benchmark of 244 open math problems drawn from Research Experiences for Undergraduates (REU) programs, formalized by experts across many math subfields.
- Motivation: as LLMs tackle conjectures at scale, verification has become the bottleneck; well-known open problems are unusable once solved and disseminated, so lower-profile REU problems suit held-out, end-to-end evaluation better.
- The team built Leanimum-agent, a minimal coding agent so all models are compared under one harness, with each problem and its logical negation placed into Lean.
- Even the best model resolves only 109 of 244 problems, highlighting the gap in end-to-end formal open-problem solving.
- Authors include Sean Welleck, Jeremy Avigad, and Prasad Tetali (arXiv:2610.27046).
More from coding & agent
- Cloudflare's "Build the next GitHub" multi-agent coding challenge finals set for Oct 21 — dinasaur_404 · 2026-10-21
- Characterizing an SG90 servo with Claude to build an accurate MuJoCo model — _Stocko_ · 2026-10-21
- Building yarrow: a shared fix library for coding agents where trust, not storage, is the hard part — Significant_Camp4148 · 2026-10-21
- mini-Lean-agent: bash-only coding agent solves 12/12 Putnam 2025 at $1.28 per problem — wellecks · 2026-10-21
- Satin: open-source React framework ships iPhone-native web apps straight from Safari — Scobleizer · 2026-10-21
- Codex now keeps prompt cache forever for logged-in users; dev says usage burn is systemic — CtrlAltDwayne · 2026-10-21