ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems
As AI systems begin to resolve open research problems, reliable verification becomes increasingly important. Formal mathematics provides a trusted framework for mathematical reasoning, enabling agents to produce machine-checkable proofs while conducting mathematical exploration. Existing formal mathematics benchmarks often focus on known results or a small set of prominent open problems, which can become difficult to evaluate reliably once solutions are discovered and widely disseminated. Existing evaluation protocols are also not always aligned with how modern coding agents operate. We therefore introduce ReuF2F, a Lean 4 benchmark of 244 formalized open problems drawn from Research Expe...
| Authors | Zeyu Zheng, Yiyang Liu, Yuyang Zhao et al. |
|---|---|
| Primary category | cs.AI |
| Published | 19 October 2026 |
| Last updated at source | 19 October 2026 |
Silytics shows public metadata from arXiv and links to the original. Information may be incomplete or out of date. Last refreshed 21 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.