cmu-l3/reuf2f 中的 ReuF2F 是一个基准，它把本科研究项目的论文和报告中的猜想以及明确提出的开放问题形式化为 Lean，以此评估编码智能体。仓库中共有244 个这类问题。未提供单独的版本或发布信息。
模型基于包含开放问题的 Lean 文件生成 patch，或者证明该定理，或者证明其完全否定。由于答案是通过检查形式化证明来判定的，评估依据的是问题是否被证明，而不是与自然语言答案的相似度。执行环境使用 Docker、固定的 elan 工具链以及 Python 3.11 及以上版本。结果按 run_id、模型名和 instance_id 分别缓存；使用相同 run_id 再次运行时会复用已保存的报告。
评估过程中会执行不可信的 Lean 代码，因此有警告要求使用不含任何凭据的临时主机。共享镜像约占 15GB，运行环境至少需要 60GB 可用空间；镜像是 linux/amd64 版本，因此在 M 系列 Mac 上需要通过模拟运行。许可证标注为 NOASSERTION，且仓库本身也没有给出性能对比结果，因此仅凭这份材料难以判断不同智能体之间的性能差异。