一句话看懂：arXiv 上出现一个名为 ReuF2F 的 Lean 4 基准，把 244 道来自本科生科研项目（REU）的开放数学问题形式化，用于评测编程智能体能否端到端给出可机器校验的证明；摘要显示最强模型也只解出约 40%。
事件核心：发生了什么
2026 年 10 月 21 日，arXiv cs.AI 收录论文 ReuF2F。作者认为，随着 AI 系统开始尝试解决开放研究问题，可靠验证变得更重要，而形式数学能提供机器可检查的证明框架。现有形式数学基准多集中在已知结论或少数知名开放问题上，一旦被解出并广泛传播，就很难持续作为“留出”评测集；评测流程也未必贴合现代编程智能体的工作方式。
因此，团队构建了 ReuF2F：从 REU 项目中收集 244 个开放问题并形式化为 Lean 4，覆盖多个数学子领域，偏向关注度较低、可能长期未解的入门级开放问题。评测采用标准编程智能体设定，把问题及其逻辑否定分别放入 Docker 容器中的 Lean 项目，并基于 mini-SWE-agent 构建 Leanimum-agent 作为统一测试框架。摘要称，表现最好的模型也只解决约 40% 的问题。
为什么重要
这指向一个更细分的评测方向：不再只考“会写代码”，而是考智能体能否在 Lean 这类可机器校验的环境中完成开放数学探索。相比知名难题，REU 开放问题曝光少、不易被训练数据覆盖，更适合作为留出测试集。统一容器和 agent harness 也试图减少不同模型比较时的工程差异。目前公开信息仅来自摘要，实验细节和评测稳定性尚待全文核验，不能据此视为永久排名。
对用户/开发者/创作者的影响
对做 AI 编程智能体、形式化数学或自动定理证明的开发者，ReuF2F 提供了一个可参考的任务形态：Lean 项目、Docker 隔离、统一 agent 框架。模型厂商若跟进，需要关注工具调用、长程推理和证明搜索能力，而不只是代码生成。对普通用户，这类基准短期不会直接变成产品功能；对内容创作者，可关注“可验证 AI 科研”这一话题，但应区分基准论文与已上线能力。
AI 工具推荐
想把多个 AI 模型放在一个入口？
GamsGo AI 集成 ChatGPT、DeepSeek、Gemini、Claude、Midjourney、Veo 等常用模型，适合写作、绘图、视频和日常 AI 工作流。
推广链接：通过此链接购买，我可能获得佣金，不影响你的价格。
值得关注的后续
一是全文是否披露各模型的具体得分、任务分布和失败类型；二是 ReuF2F 与 Leanimum-agent 是否开源、能否被社区复现；三是后续是否出现模型针对形式化开放问题做专项优化，以及基准是否会被快速污染。
来源：arXiv cs.AI
