I co-authored ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems, released as an arXiv preprint on October 19, 2026.
ReuF2F contains 244 open problems from undergraduate research, formalized in Lean 4. Coding agents work in Lean projects to prove each statement or its negation, with Lean checking the resulting proofs.
Read the paper on arXiv · Benchmark and code
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, and Sean Welleck.
arXiv:2610.27046 · Preprint · 2026