2. V2EX
  3. 陶哲轩：好问题是会被采空的资源

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

redreamality 2026-10-19 00:31 1

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


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


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

最新回复 (12)
  • 413420 10-19 00:56
    1楼
    友情提示：陶哲轩并不是无所不知的
  • sillydaddy 10-19 06:30
    2楼
    没想到啊没想到，数学竟然是首批被 AI 攻克的。唉。对普通人来说，数学多难啊！
    关键是，证明和理解这两样东西，竟然被分离开了：人类一定理解自己的证明。但机器证明的，人类则不一定理解。又一个没想到。
    如果 AI 能让人类理解所有的证明，那就不存在「资源采空」的问题了：这时的 AI 相当于人类大脑的延伸，人类知道 AI 去了哪里去过哪里。但如果 AI 的证明和人类的理解无法同步，那。。。。。。
  • xiaket 10-19 07:03
    3楼
    > "证明和理解这两样东西，竟然被分离开了"

    写 PR 和 review PR 在现在本来就是两件事情
  • horacegao 10-19 08:11
    4楼
    数学家的饭碗也被 ai 抢走了
  • kokerkov 10-19 08:18
    5楼
    @sillydaddy 数学这种强逻辑关系的，本来就更容易被机器替代吧？别忘了电脑的中文名字是电子计算机，本来就是搞数学计算弄出来的。
  • QingXuJiaZhi 10-19 08:39
    6楼
    程序员应该很容易理解这件事才对，一个问题，堆硬件暴力计算也行，在硬件受限的情况下发明一个巧妙的算法也行。

    陶哲轩的意思是，现在能把人类逼迫到不得不发明巧妙算法的“好问题”已经不多了，如果靠暴力计算去消灭这些好问题，会严重打击数学家的热情，以后就没有人去研究算法。（当然，数学与编程算法不完全一样，我这是一个方便理解的不完美类比）
  • python35 10-19 09:11
    7楼
    只能允许 ai 冲击程序员、影视行业，不能冲击数学行业么， 这么双标的么
  • levn 10-19 09:40
    8楼
    openai 还不如把 plus 的五小时限制取消。额度都缩水成什么样了。别再搞那个没用的 dots 了。难怪有人怀疑 astra 已经负责 openai 的营销，所以才这么糟糕。
  • tim9527 10-19 09:44
    9楼
    openai 推理的数学公式，有的是错误的。现在这些前端数学家都在推理。

    现有因再有果，还是先有果再看因。这是个问题
  • L4Linux 10-19 10:00
    10楼
    AI “攻克”数学难题的时候，不提 AI 有幻觉了？
  • QingXuJiaZhi 10-19 10:46
    11楼
    @python35 谁允许 ai 冲击程序员、影视行业了？各行各业都有人抗议啊。
  • cameco 10-19 10:51
    12楼
    不知道从哪本书看到的 说是数学家是最自私的那一批。
* 帖子来源V2EX
附近帖子
返回
飞读
随机推荐