AlphaProof 是 Google DeepMind 开发的自动数学定理证明系统，基于 Lean 形式化语言与强化学习结合，让 AI 能够自主搜索并写出可被机器验证的数学证明。其最新版本 AlphaProof Nexus 近期成为 AI for Math 领域最受关注的热点，标志着形式化证明系统从“应试竞赛”走向攻克真正的开放数学问题。
AlphaProof Nexus 近期进展
当前焦点与观察点
围绕 AlphaProof 的讨论主要有三个层面。其一是可靠性：由于正式同行评审信息主要来自媒体转述，学界仍在等待论文与审稿细节，以确认这些“开放问题”的难度与证明完整性。其二是科研范式之争：图灵奖得主 Richard Sutton 认为纯生成式 AI 无法做真正的科学，而 AlphaProof 这类“搜索 + 形式化验证 + 强化学习”的架构恰是对该观点的潜在反例——它依赖可验证的反馈而非纯文本生成。其三是生态外溢：类似思路已被移植到协议验证等安全领域，例如用强化学习框架加速 Tamarin 协议验证，同时开源替代方案正在快速出现。接下来值得观察的是：同行评审细节何时公开、AlphaProof 是否能转向提出新问题而非仅解题，以及低成本证明能力对数学研究工作流的实际改变。