陶哲轩：好问题是会被采空的资源

[redreamality]

最近看到一系列的 Agent 数学证明和陶哲轩的，很有感触。解决一个数学问题就像有心种花化不开，无心栽柳柳成荫

他拿自己参与的等式理论项目（ ETP ）举例。这个项目用几个月解决了 2,200 多万个泛代数蕴涵关系，并在 Lean 里形式化。有几处蕴涵卡了他们很久，逼出了构造无限反例的新技术，后来自动定理证明器发现它们其实有很小的有限反例。要是有限反例先被找到，那些更有意思的方法可能就不会出现。他的说法是，数学史上第一次，纯数学里的开放问题被当成不可再生资源来开采；开采得粗糙，数学得到的净收益会少得多。

把最近的讨论都整理了一篇博客

[413420]

友情提示：陶哲轩并不是无所不知的

[sillydaddy]

没想到啊没想到，数学竟然是首批被 AI 攻克的。唉。对普通人来说，数学多难啊！
关键是，证明和理解这两样东西，竟然被分离开了：人类一定理解自己的证明。但机器证明的，人类则不一定理解。又一个没想到。
如果 AI 能让人类理解所有的证明，那就不存在「资源采空」的问题了：这时的 AI 相当于人类大脑的延伸，人类知道 AI 去了哪里去过哪里。但如果 AI 的证明和人类的理解无法同步，那。。。。。。

[xiaket]

> "证明和理解这两样东西，竟然被分离开了"

写 PR 和 review PR 在现在本来就是两件事情

[horacegao]

数学家的饭碗也被 ai 抢走了

[kokerkov]

@sillydaddy 数学这种强逻辑关系的，本来就更容易被机器替代吧？别忘了电脑的中文名字是电子计算机，本来就是搞数学计算弄出来的。

[QingXuJiaZhi]

程序员应该很容易理解这件事才对，一个问题，堆硬件暴力计算也行，在硬件受限的情况下发明一个巧妙的算法也行。

陶哲轩的意思是，现在能把人类逼迫到不得不发明巧妙算法的“好问题”已经不多了，如果靠暴力计算去消灭这些好问题，会严重打击数学家的热情，以后就没有人去研究算法。（当然，数学与编程算法不完全一样，我这是一个方便理解的不完美类比）

[python35]

只能允许 ai 冲击程序员、影视行业，不能冲击数学行业么， 这么双标的么

[levn]

openai 还不如把 plus 的五小时限制取消。额度都缩水成什么样了。别再搞那个没用的 dots 了。难怪有人怀疑 astra 已经负责 openai 的营销，所以才这么糟糕。

[tim9527]

openai 推理的数学公式，有的是错误的。现在这些前端数学家都在推理。

现有因再有果，还是先有果再看因。这是个问题

[L4Linux]

AI “攻克”数学难题的时候，不提 AI 有幻觉了？