# reuF2F: Benchmarking coding agents on formalized undergraduate research problems

> REU F2F, a Lean 4 benchmark of 244 open problems, shows frontier AI agents resolve only ~42%, revealing a large gap in formalized mathematical research.

- **Source:** [arXiv](https://arxiv.org/abs/2610.27046)
- **Published:** 2026-10-24
- **Permalink:** https://picx.dev/p/29knE7
- **Whiteboard:** https://picx.dev/p/29knE7/image

## Summary

# 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**

| 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 |
| Oregon State University REU | 9 |
| Cornell Mathematics REU | 8 |
| University of Michigan REU | 7 |
| Budapest Semesters in Mathematics REU | 7 |
| Other REU programs | 104 |
| **Total** | **244** |

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**

| 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 |

### 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)

| 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** | **high** | **42.42** | **44.67** | **25.00** | **19.67** | **300.75K** | **83.3** |
| GPT-6 Astra | low | 7.79 | 10.25 | 2.87 | 7.38 | 4.45K | 30.9 |
| GPT-6 Astra | max | 34.63 | 37.70 | 17.21 | 20.49 | 34.92K | 23.5 |
| GPT-6.1 Sol | max | 39.55 | 40.98 | 19.26 | 21.72 | 107.18K | 53.3 |

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**

| 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 |
| Qwen3.8-Max | max | 6.76 | 9.02 | 2.05 | 6.97 | 823.93K | 178.5 |
| Gemini 3.8 Flash | high | 6.15 | 7.38 | 1.23 | 6.15 | 214.15K | 196.8 |

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

---

_Markdown view of https://picx.dev/p/29knE7, served by PicX — AI-generated visual whiteboard summaries of research papers._