FineEnvs/openai-math 数据集
将 OpenAI 数学 Lean 题目移植为 Harbor 环境用于证明任务。
为什么重要
为研究 Lean 证明生成和严格验证的 Agent 提供可用环境。
阅读原文huggingface.co
AI 解读（根据原文生成）
FineEnvs/openai-math 是 Hugging Face 上的数据集，将 OpenAI 的 openai/math release 中的数学问题移植为 Harbor environments。该数据集基于 commit `adc7f12`，包含 369 个已在环境中端到端验证官方证明的环境，覆盖 214 个结果家族和 17 个领域。任务中，Agent 在带 Lean 4 和预构建 Mathlib、无互联网的沙箱中补全 Lean 证明；完成后由 Comparator 在新沙箱中严格检查。数据集无需申请访问，许可证为 apache-2.0。
要点（AI 据原文整理，数字均已与原文核对）
- 该数据集基于 OpenAI 的 openai/math release 的 commit `adc7f12`。
- The release formalizes 405 of its results as Lean statements.
- This dataset contains 369 environments.
- 数据集覆盖 214 result families across 17 fields.
- 任务沙箱包含 Lean 4 和预构建 Mathlib，且无互联网。
- 奖励为 1 或 0：只有原始陈述完全一致、无 leftover `sorry`、无新公理且 Lean kernel 接受时得 1。
