OpenAI数学能力或源于Lean强化学习环境

如果你好奇 OpenAI 是怎么做到那些数学能力的，原因大概就在这里。他们用 Lean 形式化数学题，创建了大量强化学习环境。一开始他们可能是手工创建一些较简单的环境，但后来模型已经足够强大，可以自主创建环境，于是他们就能基于 arXiv 论文批量生成大量题目了。