Advertisement V2EX › 数学 陶哲轩：好问题是会被采空的资源 redreamality · 8h 2m ago · 414 views 最近看到一系列的 Agent 数学证明和陶哲轩的，很有感触。解决一个数学问题就像有心种花化不开，无心栽柳柳成荫 他拿自己参与的等式理论项目（ ETP ）举例。
这个项目用几个月解决了 2,200 多万个泛代数蕴涵关系，并在 Lean 里形式化。有几处蕴涵卡了他们很久，逼出了构造无限反例的新技术，后来自动定理证明器发现它们其实有很小的有限反例。
要是有限反例先被找到，那些更有意思的方法可能就不会出现。他的说法是，数学史上第一次，纯数学里的开放问题被当成不可再生资源来开采；开采得粗糙，数学得到的净收益会少得多。
把最近的讨论都整理了一篇 博客 数学 问题 资源 5 replies • 2026-10-19 08:18:43 +08:00 1 413420 7h 37m ago via iPhone 友情提示：陶哲轩并不是无所不知的 2 sillydaddy 2h 3m ago 没想到啊没想到，数学竟然是首批被 AI 攻克的。唉。
对普通人来说，数学多难啊！关键是，证明和理解这两样东西，竟然被分离开了：人类一定理解自己的证明。
但机器证明的，人类则不一定理解。又一个没想到。
如果 AI 能让人类理解所有的证明，那就不存在「资源采空」的问题了：这时的 AI 相当于人类大脑的延伸，人类知道 AI 去了哪里去过哪里。但如果 AI 的证明和人类的理解无法同步，那。
。 。
。 。
。 3 xiaket 1h 30m ago > "证明和理解这两样东西，竟然被分离开了" 写 PR 和 review PR 在现在本来就是两件事情 4 horacegao 23 mins ago 数学家的饭碗也被 ai 抢走了 5 kokerkov 15 mins ago @ sillydaddy 数学这种强逻辑关系的，本来就更容易被机器替代吧？
别忘了电脑的中文名字是电子计算机，本来就是搞数学计算弄出来的。