数学家怕 AI 写出千页证明，结果它只写了 15 页
人类反证一个关于随机图的猜想，用了 250 页、还建立在另外 200 页之上；AI 在群论内部十几页就证出了更弱的那个结论。AI 的数学证明普遍短而优雅，长证明反倒只有人类写得出来。
原视频在 YouTube 上放不出来，用音频听：
核心论点 · 点时间戳可跳到原声
模型最先替代的是文献检索
Erdős 留下的问题被整理成一个网站，标着 open 的题目未必真的还没解决——数学文献本身很难搜。一位嘉宾盯着其中一道没有把握，把题目丢进 GPT-5，五分钟后模型给出了一篇参考文献，等于告诉他这题够得着、这么做就行。而他和几个朋友已经在这道题上花了好几个小时，还不确定是否做得出来。他们随后又找出十来个同类案例。模型的第一块阵地不是证明，而是数学家最耗时的检索与细节执行。
模型不是更聪明，是更敢下注
人类数学家的日常是「和问题赌博」：有个想法，觉得可能行，试几个小时、几天、几周，然后放弃；一两年后得知别人把你想过的思路做通了。模型的差别不在灵感，而在于它不计算风险回报——人类让它做，它就做到底。而且它并非穷举：它试很多不同的路，非常执着，但只能试有限的想法，靠已有知识加数学判断把搜索树剪掉。unit distance 问题里，思路可能早就有人想到，真正难的是把极其琐碎的执行细节全部对齐，而那部分人类容易迷失，模型几乎不出错。
人会被自己的思路污染，模型不会
人类一旦沿着错误路线走了一阵，最早那个想法就和后来失败的东西绑在一起——用嘉宾的话说，上下文窗口被污染了，你没法从上周的自己身上克隆一个干净的会话出来，说别做这个、换个方向重建直觉；模型可以，大不了重开一局。它更新「这条路有多大概率走通」的方式也更像计算：人类第一次失败就会自动下调对方法的信心，模型似乎更擅长反复调整概率，而不是直接把一条路毙掉。所以它其实也在回溯和犯错，只是不会因此被拖住。
模型把数值猜测补成了等号
球堆叠问题只有 1、2、3、8、24 这五个维度有精确答案；3 维的证明最短也有几百页，出了名的丑陋。长期最好的上界来自 1970 年代两位俄罗斯数学家的两页论文，常数是 2 的 -0.599d 次方——那是某个极其丑陋的优化问题的解。Viazovska 的线性规划框架只在 8 维和 24 维恰好取到最优，这也是她拿到 Fields Medal 的重要原因。模型做的不是把常数算小一点，而是证明这套框架在大维度下的最优值本身就是那个漂亮的渐近式：是等号，不是不等式。一位嘉宾读博时在这题上想过约六个月、零进展，最后看到模型用几页复分析把它补完。
一句「再推一步」换来一个猜想值
十个问题里，只有球码与二元码这一对是有交互的：他们先让模型用表示论改进码的界，模型做到就停下；于是他们追问能不能再往前推，模型给出了复杂得多的表示论版本，而把这条路推到极限，竟然还原了球堆叠在大维度下的那个猜想值——两项工作不是巧合，而是同一个方法的两端。这也引出主持人的疑问：这是模型缺判断力，还是 harness 的问题？嘉宾的答案是任务导向：它做完你交代的事就收工，不是能力不够，再问一次它就走得更远。
不是推不动，是没被要求推
更诚实的一句总结是：这不是能力问题，它当时就是不想做。任务导向是一把刀的两面——模型会把你交代的事做到，然后停下；有时它明明已经意识到自己做出了突破，也不会主动推到极限，因为那不是你问的。由此引出 taste 的讨论：有人给出功利版本的定义，能靠更好的判断更快解决问题就是 taste；也有人认为 taste 是知道哪些问题、哪些方法值得投入。一个折中方案是拆开：让一个模型负责 taste，另一个当它的下属去做长时程的苦工，两者不必共享上下文，也就不用互相污染。
AI 十几页做到人类几百页的事
sofic 群粗略说就是能被有限群逼近的群，此前没人知道非 sofic 群是否存在。更强的一个猜想（Aldous–Lyons）两年前刚被推翻：那份工作被称为 tour de force，250 页，还建立在另外 200 页之上，动用了量子复杂度理论，能读懂的人不多。而证明存在非 sofic 群这个更弱的结论，模型只用了大约 15 页，全程留在群论里，只借用了一些已有的群论结果。嘉宾说，一年前他会以为 AI 的证明会是一千页看不懂的东西，结果恰恰相反——现在只有人类写得出两百页的证明。
证明不再是瓶颈，理解才是
过去的逻辑是：证明一个结果太难，所以后面的理解、吸收、解释都顺带完成——你自己证出来的东西，自然理解得透，也自然负责讲给别人听。现在证明这块瓶颈被大幅削掉，理解、把结果放进恰当的框架、向其他人解释，反而成了显性的、会被奖励的贡献。但天花板还在：数学问题的难度上限很高，即使模型继续指数式变强，P versus NP 这类问题可能永远不会被解决。所以数学更可能围绕这些大谜题组织，小谜题交给机器——顺便，模型既生产指数级更多的数学，也让吸收变快，它在解决自己制造的问题。
原话 · 已逐字校验
It's not really trying everything. It tries a lot of different things. It's extremely dogged.
它并不是真的在穷举。它试很多不同的东西，而且极其执着。
It's sort of like your context window is a little polluted, and you can't just make another clone of yourself from last week and say, don't do this, try something else, build your intuition in another direction.
有点像你的上下文窗口被污染了一点，你没法把自己上周的克隆体调出来说：别做这个，换个方向，重新建立你的直觉。
I had actually thought about this problem for about six months at some point when I was a graduate student. And, yeah, I just, I remember making, like, absolutely zero progress on it.
这道题我读博的时候其实想过大概六个月，我记得自己完全没有任何进展。
So it wasn't like a capabilities issue. It just didn't feel like it at the time.
所以这不是能力问题。它当时就是不想做。
It was like 250 pages building on another 200 pages. It uses like quantum complexity theory.
那是 250 页的论文，还建立在另外 200 页之上。它用到了量子复杂度理论。
It's like 15 pages maybe. And it doesn't have any of this like very complicated connection with quantum complexity.
大概 15 页。而且完全不需要和量子复杂度那套非常复杂的东西挂钩。
Only humans can generate 200-page proofs right now.
现在只有人类才写得出 200 页的证明。
I mean, a nice thing about math is that the ceiling for difficulty of a math problem is pretty high.
我的意思是，数学的一个好处是，数学问题的难度天花板非常高。
数字与实体
| GPT-5 找到一篇参考文献所花时间 | 5 分钟 | 4:08 |
| 同类的文献检索成功案例 | 又找到 10 个 | 4:08 |
| 参与 Astra 的公开问题数 | 10 个 | 15:18 |
| 3 维球堆叠最短证明长度 | 几百页 | 17:22 |
| 球堆叠有精确答案的维度数 | 5 个（1、2、3、8、24 维） | 18:23 |
| 球堆叠长期最优上界的常数 | 2 的 -0.599d 次方 | 20:27 |
| 模型给出的线性规划界渐近常数 | 约 2 的 -0.601…d 次方 | 22:27 |
| Aldous–Lyons 猜想人类反证篇幅 | 250 页，另建立在 200 页之上 | 50:57 |
| AI 证明存在非 sofic 群的篇幅 | 约 15 页 | 51:57 |
术语
- sphere packing球堆叠
- 在 d 维空间里求球体的最密排列，是经典几何难题。
- linear programming bound线性规划界
- 构造一个满足两条性质的函数，把球堆叠密度转成可优化的上界。
- spherical code球面码
- 把球堆叠搬到球面上，等价于研究纠错码的码率极限。
- sofic groupsofic 群
- 能在某种意义上被有限群逼近的群；此前不知道非 sofic 群是否存在。
- Aldous–Lyons conjectureAldous–Lyons 猜想
- 任何满足 unimodularity 的无限随机图都能被大有限图逼近。
- harness外围编排
- 模型之外由人设计的提示、工具与训练流程，共同决定最终表现。
收听指南
做 AI 应用或投资的读者，尤其是想判断「模型是不是只会暴力搜索」的人；以及关心科研工作流会被怎么改写的研究者。
[43:45] 起讲「什么是群」的入门铺垫可以快进。