主要来源AIGCLINK
查看原文事件专题 ·多源确认
Hugging Face 将 OpenAI 数学成果转为开源 RL 训练环境
Hugging Face 把 OpenAI 近期公布的数学成果改造成开源强化学习环境，共包含 369 个任务、405 道形式化数学题和 214 个题型。每个任务提供一份带 sorry 的 Lean 题面，模型需要补全成完整证明。环境内置独立沙箱中的 Lean 判分器，自动编译验证，答对记 1、答错记 0，reward 可直接用于训练。目前 verifier 只认原始形式化写法，等价证明可能被误判，项目还处于早期版本。
当前结论
Hugging Face 把 OpenAI 的数学题搬进了开源 RL 环境，405 道 Lean 形式化题自动判分，接进训练流程就能让模型自己刷题学证明。
11 个信源52° AI 热度最后更新 2026/10/12 08:34:36
证据链
11 个信源冲突核查
现有去重数据只说明这些来源讨论同一事件，不代表立场相同。当前没有结构化的支持或反驳证据，不自动推断冲突。