Overview
Field: NLP Authors: Zeyu Zheng, Yiyang Liu, Yuyang Zhao, Congmin Zheng, Jiachen Zhu, Jianian Chen, Kangning Zhang, Kayue Daniel Wong, Lingyu Yang, Rong Shan, Shihao Chen, Thomas Zhu, Wentao Zhang, Xiaopeng Li, Yan Hu, Yongxi Lin, Yuxiang Chen, Zhuoying Ou, Jianghao Lin, Jeremy Avigad, Prasad Tetali, Jingbang Chen, Sean Welleck Published: 2026-10-22 arXiv: 2610.27046
Summary
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.
However, existing formal mathematics benchmarks typically focus on known results or a small set of prominent open problems, which 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.
Key Contributions
- ReuF2F benchmark: A Lean 4 benchmark of 244 formalized open problems drawn from Research Experiences for Undergraduates (REU) programs, spanning entry-level open research problems across a broad range of mathematical subfields.
- Held-out evaluation rationale: These less well-known open problems tend to receive less attention and may remain unsolved longer, making them better suited for end-to-end held-out evaluation of open-problem solving in Lean.
- Standard agent setup: Each problem, along with its logical negation, is placed into a Lean project inside a Docker container, following standard coding-agent evaluation practices.
- Leanimum-agent: Built on mini-SWE-agent, providing a unified harness for fair comparison across models.
Findings
Even the best-performing models solve only about 40% of the problems, leaving substantial room for improvement in solving formalized open research problems.
--- *Auto-collected on 2026-10-22*