ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems
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
Organizations: Carnegie Mellon University · Chinese University of Hong Kong, Shenzhen · Shenzhen Loop Area Institute · Shanghai Jiao Tong University · Yau Mathematical Sciences Center, Tsinghua University · University College London
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.
Figures & tables
Figure 1: reuF2F draws its task instances from open problems in undergraduate research projects, formalized in Lean. Given a snapshot of the Lean workspace, coding agents generate patches that are evaluated by Comparator using both the Lean kernel and nanoda.
Benchmark
# Tasks
Setting
Formalized?
Open?
Diverse subfields?
Lower leakage risk?
AIME
30
Competition
✗
✗
✗
✗
IMO-Bench ( Luong et al., 2025 )
400/60/1,000/60
Competition
△
✗
✗
✗
MathArena Apex ( Dekoninck et al., 2026 )
12
Competition
✗
✗
✗
✗
ArXivMath ( Dekoninck et al., 2026 )
30/48
Research
✗
✗
✓
✗
First Proof ( Abouzaid et al., 2026a ; Abouzaid et al., 2026b )
10/10
Research
✗
△
✓
✓
Soohak ( Son et al., 2026 )
439
Research
✗
△
✓
✓
Table 1: Comparison with representative mathematics benchmarks.
Source program
# Problems
University of Minnesota Duluth REU
34
Williams College SMALL REU
24
University of Minnesota Twin Cities REU
16
Polymath Jr.
14
MIT SPUR
11
Yale SUMRY
10
Table 2: Problem counts by source program in reuF2F .
Method
What is checked
Errors addressed
lake build
Elaboration and compilation
Syntax, elaboration, and type errors
+ Axiom checking
Dependency
Unauthorized axioms
+ SafeVerify
Specification
Type manipulation
+ Comparator
Sandboxed export and kernel replay
.olean -level attacks
+ nanoda
Independent kernel checking
Lean kernel bugs
Table 3: Verification layers and the invalid submissions they are designed to detect
Figure 2: Test-time scaling results. Thin lines show pass@1 (one attempt), thick lines show pass@2 (two attempts on each problem), with twice the average token budget for the same configuration. Labels indicate reasoning effort.
Model
Effort
pass@1
pass@2
proved@2
refuted@2
Avg. out tokens
Avg. steps
Claude Opus 5.5
low
9.22
13.52
6.56
6.97
11.26K
12.9
Claude Opus 5.5
medium
23.16
28.28
13.52
14.75
40.68K
30.5
Claude Opus 5.5
high
29.30
35.66
18.85
16.80
62.81K
27.4
Claude Opus 5.5
xhigh
35.66
39.34
20.90
18.44
120.10K
36.7
Claude Opus 5.5
max
42.01
43.85
23.36
20.49
230.18K
53.4
Gemini 4 Argon
low
36.27
42.62
24.18
18.44
238.10K
86.7
Table 4: Reasoning-effort scaling on the full benchmark. All resolution metrics are percentages.
Model
Effort
pass@1
pass@2
proved@2
refuted@2
Avg. out tokens
Avg. steps
Gemini 4 Argon
high
42.42
44.67
25.00
19.67
300.75K
83.3
Claude Opus 5.5
max
42.01
43.85
23.36
20.49
230.18K
53.4
GPT-6.1 Sol
max
39.55
40.98
19.26
21.72
107.18K
53.3
GPT-6 Astra
max
34.63
37.70
17.21
20.49
34.92K
23.5
GPT-6 Sol
max
18.03
19.26
6.97
12.30
335.55K
255.6
Kimi K3
max
7.17
9.84
2.87
6.97
499.78K
132.9
Table 5: Model comparisons on reuF2F . Tokens and step counts are averaged over all attempts.
Figure 3: Cost/performance Pareto frontier. Each point is one model–effort configuration. The dashed lines indicate the Pareto frontier.
Figure 4: Number of problems resolved under pass@2 by the four frontier models. Each subject area contains 45 problems, except for “Others”, which contains 19. Solid segments denote proved problems; hatched segments denote refuted problems. Numbers above the bars give the totals.
Large language models (LLMs) increasingly excel at mathematical reasoning, but their unreliability limits their utility in mathematics research. A mitigation is using LLMs to generate formal proofs in languages like Lean. We perform the first large-scale evaluation of this method's ability to solve open problems. Our most capable agent autonomously resolved 9 of 353 open Erdős problems at the per-problem cost of a few hundred dollars, proved 44/492 OEIS conjectures, and is being deployed in combinatorics, optimization, graph theory, algebraic geometry, and quantum optics research. A basic agent alternating LLM-based generation with Lean-based verification replicated the Erdős successes but proved costlier on the hardest problems. These findings demonstrate the power of AI-aided formal proof search and shed light on the agent designs that enable it.
George Tsoukalas, Anton Kovsharov, Sergey Shirobokov +18
As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures, an evolving benchmark of currently 2615 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1029 open research conjectures providing a zero-contamination benchmark for mathematical proof discovery, and 836 solved problems for proof autoformalization. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged to make new mathematical discoveries, including the resolution of open research conjectures. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.
Moritz Firsching, Paul Lezeau, Salvatore Mercuri +8
Google DeepMind · Imperial College London · Stockholms universitet +1
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.
Nikil Ravi, Kexing Ying, Vasilii Nesterov +5
Vals AI · École Polytechnique Fédérale de Lausanne (EPFL) · Moscow Institute of Physics and Technology +2