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