As AI systems begin to tackle open research questions, reliable verification becomes increasingly critical. Formal mathematics offers a trusted reasoning framework that lets agents produce machine‑checkable proofs while exploring mathematics. Existing formal‑math benchmarks mainly target known results or a handful of high‑profile open problems; once these are solved and widely disseminated, evaluation becomes problematic. Moreover, current evaluation protocols often do not align with how modern coding agents operate.
To address this, we introduce ReuF2F, a Lean 4 benchmark comprising 244 formalized open problems drawn from Research Experiences for Undergraduates (REU). The problems span a broad range of mathematical subfields and represent entry‑level research challenges that receive less attention, making them well‑suited for held‑out end‑to‑end evaluation of open‑problem resolution in Lean.
In a standard coding‑agent evaluation setting, each problem and its logical negation are placed into a Lean project inside a Docker container. We build Leanimum‑agent on top of mini‑SWE‑agent to provide a unified harness for fair model comparisons.
Our evaluation finds that even the best‑performing model solves only about 40% of the problems, leaving substantial room for improvement on formalized open research problems.
Review: ReuF2F offers a more challenging and enduring test suite for assessing coding agents’ capabilities in genuine mathematical discovery, suggesting future work should focus on deeper reasoning and proof‑search strategies.