@sudheerdotai Leanimum-agent (cmu-l3/Leanimum-agent) is a fully functional coding agent, so it has access to all bash inputs and outputs, including Lean checker errors, and can iteratively debug its proofs!
9 views
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 Experiences for Undergraduates (REU), spanning entry-level open research problems across a broad range of mathematical subfields. We expect these less prominent open problems, which tend to attract less attention and may remain unsolved for longer, to be better suited for held-out evaluation of end-to-end open problem resolution in Lean. We adopt a standard coding-agent evaluation setting, placing each problem and its logical negation into a Lean project in a Docker container. We also build Leanimum-agent on mini-SWE-agent to provide a unified harness for fair comparisons across models. Our evaluation finds that even the best-performing model resolves only ~40% of the problems, leaving substantial room for improvement on formalized open research problems.
Comments: Benchmark available at cmu-l3/reuF2F
I’m honoured to be part of this project. Thanks to Zeyu @regunivers , a excellent researcher who leads the project and Jinbang @_chenjb who contributes a lot. I am happy to know many collaborators. Paper: zeyu-zheng.github.io: cmu-l3/reuF2Fagent: cmu-l3/Leanimum-agent
1 like · 42 views
Amazing work and collaborative effort led by Zeyu Zheng (@regunivers)!
Paper: zeyu-zheng.github.io
Benchmark: cmu-l3/reuF2F
Leanimum Agent: cmu-l3/Leanimum-agent (7/7)
2 likes · 1 repost · 79 views
paper: zeyu-zheng.github.io
benchmark: cmu-l3/reuF2F
agent: cmu-l3/Leanimum-agent
2/5
Why REU problems? Famous open problems (Erdős problems, Formal Conjectures) are great targets, but once one is solved the proof spreads fast, and a search agent can easily look it up.
We really want a held-out evaluation!
REU conjectures are a better fit. they are genuine open research questions, typically followed up by fewer people, so they are more likely to stay open, and unspoiled, for longer.
We collected 244 problems from Duluth, Williams SMALL, MIT SPUR, Yale SUMRY, Polymath Jr. and more. The set has 45 problems in each of combinatorics, number theory, algebra, geometry & topology, and analysis, plus 19 Others.
To preserve the benchmark's long-term utility, we encourage the community not to publicly release formalized solutions to benchmark problems.
1 like · 97 views
Mentions
@sudheerdotai Leanimum-agent (cmu-l3/Leanimum-agent) is a fully functional coding agent, so it has access to all bash inputs and outputs, including Lean checker errors, and can iteratively debug its proofs!
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 Experiences for Undergraduates (REU), spanning entry-level open research problems across a broad range of mathematical subfields. We expect these less prominent open problems, which tend to attract less attention and may remain unsolved for longer, to be better suited for held-out evaluation of end-to-end open problem resolution in Lean. We adopt a standard coding-agent evaluation setting, placing each problem and its logical negation into a Lean project in a Docker container. We also build Leanimum-agent on mini-SWE-agent to provide a unified harness for fair comparisons across models. Our evaluation finds that even the best-performing model resolves only ~40% of the problems, leaving substantial room for improvement on formalized open research problems. Comments: Benchmark available at cmu-l3/reuF2F
I’m honoured to be part of this project. Thanks to Zeyu @regunivers , a excellent researcher who leads the project and Jinbang @_chenjb who contributes a lot. I am happy to know many collaborators. Paper: zeyu-zheng.github.io: cmu-l3/reuF2Fagent: cmu-l3/Leanimum-agent
Amazing work and collaborative effort led by Zeyu Zheng (@regunivers)! Paper: zeyu-zheng.github.io Benchmark: cmu-l3/reuF2F Leanimum Agent: cmu-l3/Leanimum-agent (7/7)
paper: zeyu-zheng.github.io benchmark: cmu-l3/reuF2F agent: cmu-l3/Leanimum-agent 2/5 Why REU problems? Famous open problems (Erdős problems, Formal Conjectures) are great targets, but once one is solved the proof spreads fast, and a search agent can easily look it up. We really want a held-out evaluation! REU conjectures are a better fit. they are genuine open research questions, typically followed up by fewer people, so they are more likely to stay open, and unspoiled, for longer. We collected 244 problems from Duluth, Williams SMALL, MIT SPUR, Yale SUMRY, Polymath Jr. and more. The set has 45 problems in each of combinatorics, number theory, algebra, geometry & topology, and analysis, plus 19 Others. To preserve the benchmark's long-term utility, we encourage the community not to publicly release formalized solutions to benchmark problems.