AlphaProof 的强化学习 formal reasoning 方法在 Nature 正式发表，确立 autoformalization + RL + Lean verification 的经典范式

Google DeepMind 的 AlphaProof methodology 于 11 月 12 日在 Nature 在线发表。系统将自然语言问题 autoformalize 为 Lean statements，通过大规模 synthetic formal problems、reinforcement learning 与 proof search 训练，并由 Lean kernel 对最终 proof 做机器验证。论文系统给出 2024 IMO silver-level 结果的方法学与 ablations，使此前博客级 milestone 变成同行评审的 formal-math 研究基线。