陶哲轩：好问题是会被采空的资源
1112
- redreamality2026-10-19
最近看到一系列的 Agent 数学证明和陶哲轩的，很有感触。解决一个数学问题就像有心种花化不开，无心栽柳柳成荫
他拿自己参与的等式理论项目（ ETP ）举例。这个项目用几个月解决了 2,200 多万个泛代数蕴涵关系，并在 Lean 里形式化。有几处蕴涵卡了他们很久，逼出了构造无限反例的新技术，后来自动定理证明器发现它们其实有很小的有限反例。要是有限反例先被找到，那些更有意思的方法可能就不会出现。他的说法是，数学史上第一次，纯数学里的开放问题被当成不可再生资源来开采；开采得粗糙，数学得到的净收益会少得多。
把最近的讨论都整理了一篇博客
主楼 - 4134202026-10-19
友情提示：陶哲轩并不是无所不知的
- sillydaddy2026-10-19
没想到啊没想到，数学竟然是首批被 AI 攻克的。唉。对普通人来说，数学多难啊！
关键是，证明和理解这两样东西，竟然被分离开了：人类一定理解自己的证明。但机器证明的，人类则不一定理解。又一个没想到。
如果 AI 能让人类理解所有的证明，那就不存在「资源采空」的问题了：这时的 AI 相当于人类大脑的延伸，人类知道 AI 去了哪里去过哪里。但如果 AI 的证明和人类的理解无法同步，那。。。。。。 - xiaket2026-10-19
- horacegao2026-10-19
数学家的饭碗也被 ai 抢走了
- kokerkov2026-10-19
@sillydaddy 数学这种强逻辑关系的，本来就更容易被机器替代吧？别忘了电脑的中文名字是电子计算机，本来就是搞数学计算弄出来的。
- QingXuJiaZhi2026-10-19
程序员应该很容易理解这件事才对，一个问题，堆硬件暴力计算也行，在硬件受限的情况下发明一个巧妙的算法也行。
陶哲轩的意思是，现在能把人类逼迫到不得不发明巧妙算法的“好问题”已经不多了，如果靠暴力计算去消灭这些好问题，会严重打击数学家的热情，以后就没有人去研究算法。（当然，数学与编程算法不完全一样，我这是一个方便理解的不完美类比）
python352026-10-19只能允许 ai 冲击程序员、影视行业，不能冲击数学行业么， 这么双标的么
- levn2026-10-19
openai 还不如把 plus 的五小时限制取消。额度都缩水成什么样了。别再搞那个没用的 dots 了。难怪有人怀疑 astra 已经负责 openai 的营销，所以才这么糟糕。
- tim95272026-10-19
- L4Linux2026-10-19
AI “攻克”数学难题的时候，不提 AI 有幻觉了？
- QingXuJiaZhi2026-10-19
- cameco2026-10-19
不知道从哪本书看到的 说是数学家是最自私的那一批。