机器之心 (微信公众号)T2·68 分
九章云极言表实验室满分夺冠陶哲轩数学蒸馏挑战赛：强化学习驱动 Lean 4 形式化证明生成
原标题：九章云极问鼎陶哲轩数学挑战赛！让强化学习成为AI4S新基建
- 九章云极言表实验室在 294 支队伍中以总分 221 分、四赛道满分的成绩获得陶哲轩数学蒸馏挑战赛第一名。
- 比赛核心规则要求提交 Lean 4 形式化证明或反例，由确定性验证器检验，强调“可验证性”而非单纯“正确率”。
- 该成果表明强化学习可作为 AI for Science 的基础设施，推动 AI 从批量解题转向辅助人类进行深层数学概念理解与发现。