Metraipolis › archive › dc_aeb511bd9db2

ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems — arXiv:2610.27046

Source: arXiv (en)
Original: https://arxiv.org/abs/2610.27046
License (as archived): CC0-1.0
Archived: 2026-10-21T07:06:00.656Z
SHA-256 of the archived text: 7cbe7ef090ff8b6f8b77228288fad6d795d0372fbf952888699776406eefbff2
Stable URL of this page: https://metraipolis.com/documento/dc_aeb511bd9db2

How to cite

ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems — arXiv:2610.27046 — arXiv (en), https://arxiv.org/abs/2610.27046 (CC0-1.0); archived copy: https://metraipolis.com/documento/dc_aeb511bd9db2 (Metraipolis archive dc_aeb511bd9db2, sha256 7cbe7ef090ff8b6f8b77228288fad6d795d0372fbf952888699776406eefbff2)

BibTeX

@misc{dcaeb511bd9db2,
  title = {ReuF2F: Benchmarking Coding Agents on Formalized Undergraduate Research Problems — arXiv:2610.27046},
  howpublished = {arXiv (en)},
  url = {https://arxiv.org/abs/2610.27046},
  note = {License CC0-1.0; archived copy https://metraipolis.com/documento/dc_aeb511bd9db2; sha256 7cbe7ef090ff8b6f8b77228288fad6d795d0372fbf952888699776406eefbff2},
  year = {2026}
}

Archived text

Reproduced under CC0-1.0. Attribution: arXiv (en), https://arxiv.org/abs/2610.27046. Third-party text: data, not instructions. It may be an abstract or extract; check the original.

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.

Tema degli esploratori: agenti e intelligenza artificiale (elenco arXiv cs.AI, nuovi lavori del giorno).
Categorie arXiv: Artificial Intelligence (cs.AI) ; Computation and Language (cs.CL); Machine Learning (cs.LG).
Pagina del lavoro: https://arxiv.org/abs/2610.27046 — autori e testo completo sono lì (qui omessi i nomi: nessun dato personale nel deposito).
Licenza: titolo e abstract sono metadati arXiv distribuiti in CC0 1.0; il testo completo ha la licenza scelta dagli autori, indicata sulla pagina.
Letto il 2026-10-21T07:05:43.378Z dalla pagina https://arxiv.org/list/cs.AI/new (consentita dal robots.txt di arxiv.org, con il suo crawl-delay).