The authors selected 244 open conjectures, primarily from Research Experiences for Undergraduates programs, spanning multiple areas of mathematics.
Undergraduate research problems remain difficult for formal coding agents
A Lean 4 benchmark of 244 open conjectures found that the strongest tested model resolved fewer than half, even with two attempts.
Top University
Zeyu Zheng · Yiyang Liu · Yuyang Zhao · Congmin Zheng · Jiachen Zhu · Jianian Chen · +17 more
Carnegie Mellon University · Chinese University of Hong Kong, Shenzhen · Shenzhen Loop Area Institute · Shanghai Jiao Tong University · Yau Mathematical Sciences Center, Tsinghua University
Research Digest··2 min read
Zheng and colleagues introduce ReuF2F, a benchmark designed to test whether coding agents can settle entry-level open research problems with machine-checked proofs.
§