Summary of REU F2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems

Summary (Overview)

• New Benchmark: Introduces REU F2F, a Lean 4 benchmark containing 244 formalized open problems drawn from Research Experiences for Undergraduates (REU) programs, spanning diverse mathematical subfields including discrete mathematics, number theory, algebra, geometry, topology, and analysis.

• Two-Way Evaluation Protocol: Unlike traditional proof-only benchmarks, REU F2F allows agents to either prove or refute each conjecture, since open problems may be false. Each task includes both the original statement $\phi_i$ and its logical negation $\neg\phi_i$.

• Trusted Verification Stack: Uses Comparator with the official Lean kernel plus nanoda (an independent Rust-based type checker) to prevent adversarial submissions that exploit Lean's metaprogramming capabilities or kernel bugs.

• Standardized Harness: Builds Leanimum-agent, adapted from mini-SWE-agent, providing all models with identical task instructions, shell interfaces, and interaction loops to ensure fair cross-model comparisons.

• Key Results: The best-performing model (Gemini 4 Argon at high reasoning effort) resolves only 42.42% (pass@1) and 44.67% (pass@2) of problems, leaving substantial room for improvement on formalized open research problems.

Introduction and Theoretical Foundation

Background and Motivation

The paper addresses a critical challenge in AI evaluation: as AI systems increasingly resolve open research problems (e.g., the unit distance conjecture, Navier–Stokes blowup results), traditional verification methods become inadequate. Human verification of natural-language proofs is unreliable and unscalable.

The Role of Formal Proof Assistants

Lean 4 provides a natural bridge between mathematics and coding through the Curry–Howard correspondence, where:

• Mathematical statements are represented as types
• Proofs are represented as terms
• Correctness is checked by a trusted kernel

This allows arguments to be verified without requiring human readers to develop detailed understanding first.

Problem with Existing Benchmarks

Existing formal mathematics benchmarks (e.g., FrontierMath Erdős, Formal Conjectures) focus on famous open problems that attract substantial community attention. Once solved, solutions are widely disseminated online, and since mathematical research naturally involves literature search, agents may retrieve these solutions during evaluation—undermining their value as held-out tests.

REU as a Solution

REU programs give undergraduate students research experience through faculty mentorship. Their conjectures:

• Arise from genuine mathematical research
• Typically receive less concentrated attention than famous conjectures
• Are expected to have lower leakage risk for future evaluation

Methodology

Task Formulation

For each problem $P_i$ with formal statement $\phi_i$, the task considers both $\phi_i$ and $\neg\phi_i$. Let $s_i^+ \in \{0,1\}$ indicate whether a proof of $\phi_i$ is accepted, and $s_i^- \in \{0,1\}$ indicate whether a proof of $\neg\phi_i$ is accepted. Since both cannot be provable in a consistent system, $s_i^+ s_i^- = 0$. The resolution indicator is:

$$r_i = s_i^+ + s_i^- \in \{0,1\}$$

Problem Selection

Problems were collected from publicly available REU papers, preprints, and project reports. Each selected question was verified to:

1. Be first proposed in the source paper
2. Be central to the research contribution
3. Remain unresolved

Table 2: Problem counts by source program

Problems are organized into five balanced areas (45 problems each): discrete mathematics/combinatorics; number theory/arithmetic; algebra/algebraic geometry; geometry/topology; analysis/dynamics/probability/PDE. The remaining 19 are grouped under "Others."

Evaluation Protocol Design

The paper identifies four fundamental issues with traditional formal theorem-proving benchmarks:

1. Proof-only evaluation: Assumes propositions are provable, which is inappropriate for open conjectures
2. Trusted verification: Lean's metaprogramming allows compilation without providing intended proofs
3. Harness confounding: Different harnesses make models hard to compare
4. Environment dependence: Performance depends on hardware, files, and task ordering

Verification Layers

Table 3: Verification layers and the invalid submissions they detect

Leanimum-Agent

Adapted from mini-SWE-agent, it provides:

• Filesystem access
• Command execution
• Persistent file edits
• Iterative feedback

The prompt explains the proof-or-refutation objective, names target declarations, shows how to search Mathlib with rg, and requires checking changes with lake build before submission.

Empirical Validation / Results

Evaluation Configuration

• Lean and Mathlib: v4.34.0
• Hardware: 20 CPU cores, 60 GB RAM (identical for agent and evaluation containers)
• Limits: 1,000 agent steps, 6 hours wall-clock time, 1,200-second timeout per shell command
• Two independent attempts per model configuration on every problem

Full-Benchmark Results and Test-Time Scaling

Table 4: Reasoning-effort scaling on the full benchmark (All metrics in percentages)

Key findings:

• pass@1 and pass@2 increase monotonically with reasoning effort for all models
• Increasing effort can be more token-efficient than repeating attempts (e.g., Opus high effort achieves 29.30% pass@1 with 62.81K tokens vs. 28.28% pass@2 at medium with 81.35K tokens)

Cross-Model Comparisons

Table 5: Model comparisons on REU F2F

Notable observations:

• Substantial performance gap between open-source and proprietary models
• Open-source models (Kimi K3, Qwen3.8-Max) use more output tokens yet resolve far fewer problems
• Even the strongest configuration leaves more than half of the benchmark unresolved after two attempts

Performance Across Mathematical Areas

For all four frontier models, algebra and algebraic geometry contributes the largest number of resolutions. Gemini 4 Argon leads in "Others" (7 of 19 problems, primarily theoretical computer science and mathematical logic).

Theoretical and Practical Implications

Mathematical Verification Paradigm

The paper demonstrates a new paradigm of mathematical verification driven by machine-checkable formal proofs. This is evidenced by:

• The Polynomial Freiman–Ruzsa formalization project
• Anthropic's 11-day agent-assisted formalization of Fermat's Last Theorem
• Lean certificates accompanying recent Navier–Stokes results

Evaluation Methodology

The benchmark establishes best practices for evaluating AI mathematical reasoning:

1. Two-way evaluation (proof or refutation) is essential for open problems
2. Multi-layer verification (beyond just lake build) protects against adversarial submissions
3. Sandboxed, reproducible environments ensure fair comparisons
4. Common harnesses (Leanimum-agent) separate model capability from agent scaffolding differences

Leakage Risk Mitigation

REU-sourced conjectures offer a qualitative reduction in leakage risk compared to famous open problems, as their solutions are less likely to become widely disseminated reference answers.

Conclusion

Key Takeaways

1. REU F2F provides a challenging, reproducible benchmark for evaluating coding agents on open mathematical research problems
2. Current frontier models resolve only ~40% of problems, indicating substantial room for improvement
3. The benchmark's formal-to-formal (F2F) setup ensures that both problems and accepted solutions are entirely machine-checkable

Limitations Acknowledged

• Formalizability bias: Only conjectures statable in Lean with Mathlib are included
• Independence: Gödel's incompleteness theorem means some problems may be neither provable nor refutable within permitted foundations
• Formalization faithfulness: Some Lean statements may differ subtly from intended conjectures
• Leakage risk: Any open problem may be resolved and published at any time
• Common harness limitations: No single harness is optimal for every model

Future Directions

The authors encourage the community to:

• Refrain from publicly releasing formalized solutions to preserve benchmark utility
• Use REU F2F as a foundation for tracking AI's ability to produce new, formally verified mathematical results
• Continue improving agent capabilities on formalized open research problems