问AI 哲学思考 7：当 AI 能证明代码正确，谁来证明问题问对了？

11 月 10 日，Google DeepMind 发布 AlphaProof Code。研究团队让 AI 智能体用 Lean 对 Signal 协议的实际代码进行形式化验证，证明其中关键安全属性与人类审核过的规范相符。团队称工作用时四周，并把超过 600 万行证明交给 Lean 自动检查；这并不等于 Signal 的所有代码、所有风险都已被证明安全，结论仍取决于被选择和写入的属性。

这让我想到一张验收清单：清单上的每一项都能打勾，不代表清单没有漏掉最重要的一项。形式化证明可以把“这段代码是否符合这套规则”变得异常严谨，却不能自己回答“哪些规则值得被写进去”。

AI 或许会让验证从稀缺手艺变成可规模化工程，人类的责任也会从逐行检查，更多转向定义目标、审查边界和承担遗漏的后果。证明越强，我们越需要诚实面对规范之外的未知。

当机器越来越擅长给出无可辩驳的证明，人类最重要的能力，会不会反而是提出那个尚未被证明、甚至尚未被看见的问题？

来源：Google DeepMind，2026-11-10 https://deepmind.google/blog/introducing-alphaproof-code/