跨国深谈← 返回←AI解数学题≠理解数学

AI解数学题≠理解数学

关联

人物 Lisha Lee · Daniel Litt

公司 OpenAI · Anthropic

概念 ChatGPT · Claude · Codex · RL · Lean · 直觉 · 理论构建 · 推理能力 · Erdos 单位距离问题

这一集是 a16z 基础设施合伙人 Lisha Lee 和多伦多大学数学教授 Daniel Litt 聊 AI 在数学领域的真实能力。Daniel 是一位活跃的研究者，一直在公开追踪并评论 AI 数学能力的演变。

Daniel 目前最喜欢的一个完全由 AI 自主完成的结果，是五月中旬宣布的 Erdos 单位距离问题的解决方案 。这个结果有意思的地方在于，它不是简单的”最后一公里”——即人类做了大量深活、AI 踢最后一步——而是从一个意想不到的领域引入了已有的分类思想，证明了该领域普遍相信为真的猜想实际上是假的，随后人类数学家还拿这些想法找到了其他开放问题的反例 。不过 Daniel 强调，回头看这些 AI 产出的证明，它们的推理过程看起来非常像人类数学家，并没有什么”非人”的奇招 。

模型到底在做什么

Daniel 把目前的能力边界分得很清楚。模型非常擅长两件事：一是应用所有已知技术，二是做大规模的并行计算——比如让它同时跑十个子智能体处理一千个例子 。OpenAI 和 Anthropic 的模型在他看来能力相当，ChatGPT 只是更早变强，Claude 大概在 Opus 4.5 或 4.6 左右追上 。

但模型在几个关键维度上明显偏弱。一是直觉。

数学里很多猜想嵌在巨大的理论框架里，有大量证据支持它为真，不是靠找一个反例构造就能推翻的 。二是理论构建。

Daniel 试过让模型做理论构建，给一些提示后能做出有趣的东西，但完全自主做不到 。三是提出正确的问题。很多时候找到猜想本身比证明它难得多 。

Daniel 讲了一个自己的亲身经历。他在一个项目里想证明某个引理，所有前沿模型都做不了。

他自己做了大量例子后，找到了一个更好的表述，然后模型很快就能证明这个更强的版本 。但如果你把原来那个引理直接扔给 ChatGPT，它会吐出十页毫无洞见的暴力计算 。

那种证明虽然”正确”，但不会带来任何理解上的发现。Daniel 承认自己其实知道那种暴力证法行得通，只是不愿意去做——恰恰是因为不愿意做丑陋的证明，反而逼出了更好的结果 。

“老虎机论文”与激励机制的危险

Daniel 对当前学术激励机制发出了很直接的警告。现在一个博士后如果想找工作，最快的方式是让模型去”拉老虎机”——比如让 Codex 上网找五个代数几何里的最新猜想然后去证明。

他自己跑过这个实验，一小时就得到了三篇正确但质量很差的论文 。预印本上已经出现了同一定理、同一证明、三四篇论文在几天内同时出现的情况——显然是有人在玩老虎机 。

更深层的问题是，这可能导致数学探索的多样性崩塌。数学的很多进展来自于一千个不同的人追求各自的好奇心，知识边界在高维空间里以相对均匀的方式扩展，然后突然某个新想法被引入，级联式地解决一堆老问题 。

如果数学探索从属于模型想追求的东西，你得到的可能不是一个有一百万种不同直觉的数学家群体，而是一个被复制了一千次的同一个数学家 。模型的直觉从哪来？目前还是来自人类数学家 。

Daniel 的核心论点是：数学的目标不是产出论文，而是产生理解。如果理解只存在模型权重里，对他来说”相当不令人满意” 。

维持一个有广泛兴趣、有能力在前沿有意义地参与的人类数学家群体，需要庞大的基础设施和人才管道 。如果激励机制不改变，这条管道就会断裂。

为什么模型只能产出”短巧”证明

最近一些引人注目的 AI 证明都相对简短。Daniel 的判断很直接：不是因为短证明更好，而是因为模型目前还做不到长的 。

让它生成长证明，它可能自己都不知道哪里错了 。有人贴过一篇 800 页的 AI 生成证明，Daniel 说那不可能正确——当前模型的能力范围是校准过的，而且肯定没有人类读过、模型也检查不了 。

人类检查长论文的方式不是逐行看，而是理解论证的全局结构，做各种压力测试——比如”这个论证会不会推出某个我知道是假的东西”。这种”模糊单元测试”式的宏观检查，模型目前也做不好 。

本集带走

• 模型强在应用已知技术，弱在创造新理论：它能从其他领域搬来你没读过的技术，但在需要发展全新理论框架的问题上几乎无能为力。
• “丑证明”有时是逼出好理解的起点：Daniel 的案例说明，模型直接给的那个暴力证法虽然正确但无洞见；恰恰是模型做不了、人也不愿意做的丑证明，逼出了更好的概念性解释。
• 警惕”老虎机论文”摧毁激励机制：用模型批量生产正确但无理解的论文，既不发展人力资本，也可能让数学前沿的多样性坍缩成一个模型的副本。
• 短证明不是审美选择，是能力限制：模型目前产不出可靠的长证明，因为自身还缺乏对长论证进行全局一致性检查的能力。
• 用 AI 要”上升”而非”让渡”：用模型加深自己的理解，而不是把思考外包给模型——后者太容易了，而模型其实并不能真正思考 。

话虽如此，数学的目标并不是产生数学论文。
That said, the goal of mathematics is not to produce mathematics papers.
—— Daniel Litt · [34:48]

你可以拿 Codex。你可以说，上网找五个代数几何中最近的猜想并证明它们。
You can take Codex. You can say, go online and find five recent conjectures in algebraic geometry and prove them.
—— Daniel Litt · [36:44]

它们不生成长长的、复杂的证明的原因是它们做不到。
The reason they’re not producing long, complicated proofs is that they cannot.
—— Daniel Litt · [52:47]