随着 AI 系统开始解决开放的研究问题，可靠的验证变得愈发重要。形式化数学提供了一个可信的推理框架，使得代理能够在进行数学探索的同时生成机器可检验的证明。现有的形式化数学基准大多聚焦已知结果或少数著名的开放问题，一旦这些问题被解决并广泛传播，评估就会变得困难。评估协议也往往与现代编码代理的工作方式不匹配。
为此我们推出 ReuF2F，这是一个基于 Lean 4 的基准，收录了 244 个来源于本科研究经历（REU）的形式化开放问题，覆盖多个数学子领域的入门级研究挑战。相较于热门问题，这些不太受关注的问题更适合作为端到端开放问题求解的 held‑out 评估。
在标准的编码代理评估设置下，我们将每个问题及其逻辑否定放入 Docker 容器中的 Lean 项目。我们基于 mini‑SWE‑agent 构建了 Leanimum‑agent，提供统一的实验框架，以便在不同模型之间进行公平比较。
实验结果显示，即使是表现最好的模型也只能解决约 40% 的问题，表明在形式化开放研究问题上仍有大量提升空间。
点评：ReuF2F 为评估编码代理在真实数学探索中的能力提供了更具挑战性和长期价值的测试集，未来工作可围绕模型的推理深度和证明搜索策略展开。