OpenAI 用内部前沿模型推进数学开放问题，Lean 证明已放上 GitHub

OpenAI 公布了关于数学开放问题的新研究结果，这些结果来自一个内部前沿模型。公司同时把 Lean 形式化证明以及更多研究细节放到了 GitHub 上，让数学家和开发者可以检查和在此之上继续推进。 这一动作属于更大布局的一部分：把高级 AI 系统定位成数学发现与验证的工具。OpenAI 使用 Lean 这个形式化证明助手，是想让模型的推理变得可检查，而不只是有说服力。这个区别很关键。数学命题可以被机械验证，所以形式化证明能更严格地检验 AI 到底是真找到了有效论证，还是只是写出了看起来很像样的文本。把证明和代码公开，也是在邀请外部审视，这有助于研究者发现其中的错误、取巧之处或没有明说的假设。 这次公告同时引发了热情和担忧。支持者把 AI 看作强大的协作者——它能探索巨大的搜索空间、提出猜想、帮助把人类的直觉形式化。批评者则担心署名与贡献归属、可靠性，以及机器参与到未解问题中会带来的更广泛后果。如果 AI 系统越来越多地产出新的数学知识，那么成果如何归属、如何评审、如何纳入学术实践，都会成为问题。也有人担心前沿实验室会在引导数学研究方向上获得过大的话语权。 就目前而言，OpenAI 这次发布更适合被理解成一次演示，也是一份邀请。它展示了 AI 有可能加速形式化推理，但同时也暴露出对谨慎验证和社区监督的需求。数学家们很可能会一行一行地检验这些证明，而他们的反应，将在很大程度上决定 AI 多快能成为数学发现中的常规一环。