Hugging Face 开源数学强化学习训练环境

Hugging Face 将 OpenAI 近期发布的数学成果转化为开源强化学习环境，包含 369 个任务、405 道形式化数学题和 214 个题型。该环境通过独立沙箱中的 Lean 判分器编译验证证明，给出 0/1 的 Reward 反馈，驱动模型针对特定题型迭代练习。目前工具处于早期阶段，对证明风格有特定要求，存在误判可能。