OpenAI Math 是由 FineEnvs 于 2026 年发布的一个将 OpenAI 数学结果整理为 Lean 形式化定理证明环境的数学定理证明数据集，旨在为智能体提供可严格验证的形式化数学定理证明任务。

该数据集包含 369 个通过端到端验证的 Harbor 任务环境，来源于 OpenAI openai/math 项目中形式化为 Lean 定理陈述的 405 条结果，覆盖 214 个结果家族和 17 个数学领域。

数据集采用实验性验证筛选机制，仅收录 OpenAI 原始证明能够在对应环境中通过验证的任务。智能体需要在预配置 Lean 4 和 Mathlib 的沙箱环境中，补全以 sorry 标记的证明占位符，完成原始定理的完整证明。

任务完成后，验证器会在独立沙箱中检查证明结果：要求定理陈述与原始版本完全一致，不存在未完成的 sorry，仅使用 Lean 标准公理，且证明通过 Lean 内核验证。验证通过后获得奖励 1，否则获得奖励 0。

每个任务默认配置为 4 核 CPU、8 GB 内存、10 GB 磁盘空间，执行时限为 4 小时。

数据集组成

• tasks 目录：每个通过验证的问题对应一个 Harbor 任务，包含任务说明、Lean 定理语句、沙箱镜像配方、验证器和参考求解器。
• registry.json：Harbor 注册表条目 [email protected]。
• manifest.parquet：每个任务一行，字段包括领域、结果家族、定理名称、参考证明规模和 oracle result。
• generator 目录：构建沙箱镜像并从 openai/math 重新生成任务所需的代码。
• LICENSE、NOTICE 和 LICENSE-openai-math：许可与归属说明。