ReuF2F Benchmark Using Lean 4 for Undergraduate Research Problems
October 21, 2026
ReuF2F introduces a Lean 4 benchmark consisting of 244 formalized open mathematical problems sourced from undergraduate research programs. This dataset provides a harder, less saturated evaluation path for coding agents compared to existing formal math benchmarks by focusing on less prominent, unsolved research questions.
HOW THIS AFFECTS YOU
●
researcherYou can use this to evaluate agents on genuine mathematical reasoning rather than pattern matching known proofs.