Column|LLM: 重走围棋之路

棋手和程序员的经历，或许预示着数学家的未来

两年前，最先进的 AI 模型还会犯令人尴尬的低级错误：算不对简单的算术，还信誓旦旦地告诉用户，9.11 比 9.9 大。如今，数学家正在研究 AI 生成的证明，判断它们是否解决了困扰人类数十年的难题。从课堂习题走到研究前沿，AI 只用了很短的时间。

10 月初，硅谷流传着一个消息：OpenAI 即将公布约 400 份堪比菲尔兹奖水平的数学证明。菲尔兹奖是数学界的最高荣誉之一。10 月 6 日，这批论文正式发布，数量甚至超过了传闻：722 篇手稿，分为 372 组相关研究成果，均由 OpenAI 的内部模型产出。公司称，评估期间向模型提出了约 4,000 个开放问题。按其公布的口径，每项成果平均消耗的算力约相当于 ChatGPT Pro 思考三小时；其中少数研究采用了不同的流程。

OpenAI 首席执行官 Sam Altman 特别提到了四项成果：拟黎曼猜想的证明、理论计算机科学中唯一博弈猜想的证明、霍奇猜想在 CM 阿贝尔簇上的特例，以及一个自 1940 年代以来悬而未决的自由群因子问题。霍奇猜想是七大千禧年难题之一。Altman 谨慎地将这些成果称为有待外部数学家确认的研究主张。许多证明附有 Lean 版本，但并非全部都有。Lean 是一种可以让计算机逐步核查形式化证明的语言。形式验证仍需确认所证明的命题与原问题一致。

现在就为数学家这个职业写讣告，还为时过早。“菲尔兹奖水平”算不上公认的衡量单位，这批成果也仍有待独立审查。不过，AI 能力进步的趋势已很难忽视。

我们认为，数学正在迎来自己的 AlphaGo 时刻：学科继续向前，机器逐渐成为衡量研究能力的参照，数学家也将像棋手一样，学习适应这种变化。