哀悼，还是不哀悼？
文章摘要
本文作者是帝国理工学院数学家、Lean 形式化运动的主要推动者凯文·巴扎德（Kevin Buzzard），发表在他的 Xena Project 博客上。这一篇的上一篇标题是《FLT：Anthropic 抢在我前面了》。巴扎德开篇就说，AI 数学领域最近的事件已经无可置疑地表明，这个领域正经历前所未有的剧变：语言模型在解决人类解决不了的难题。他本人对此非常兴奋，但发现很多同行显然很难过，于是先梳理了他们的立场。
悲观者与”哀伤五阶段”。 他借用库伯勒-罗斯的哀伤模型（否认、愤怒、讨价还价、抑郁、接受），认为前四个阶段在数学界都有充分体现，同时声明”不是所有人都在哀悼”，也无意批评任何一方。
- 否认：”人类数学协会”以保护数学这项人类事业、抵御”AI 威胁”为宗旨，会员承诺不发表 AI 生成的成果，还可以选择完全不在研究中使用 AI。菲尔兹奖得主彼得·朔尔策（Peter Scholze）在海德堡获奖者论坛上表示自己不会用 AI，并愿意做那个”死守这座山头的公众人物”。
- 愤怒：Proofs and Prompts 网站上能看到不少愤怒的文章。
- 讨价还价：一个包括三位菲尔兹奖得主的资深数学家顾问小组发表建议，回应 OpenAI 手握”大量由内部模型产生的重要数学成果”的消息，要求前沿实验室不要再用专有模型测试高等数学难题，并”负责任地”发布结果，资助人类对 AI 数学成果的理解工作。
- 抑郁：一位研究流体的教授称纳维-斯托克斯问题的消息”极其令人沮丧”；一位博士后考虑离开研究；一位博士生卡在某个引理上，结果 ChatGPT 一次就解决了，让他怀疑这一切还有什么意义。
人类为什么做数学？ AI 能证明难定理之后，数学家们开始强调，大奖从来是颁给带来最深刻理解的人，常引用的依据是瑟斯顿 1994 年的文章《论数学中的证明与进步》，陶哲轩的博客也把其中一句放在了页首。巴扎德认为，说数学家在”挪球门”并不公平：怀尔斯等人对费马大定理的证明，既解决了一个没什么应用的三百五十年老谜题，也给朗兰兹纲领带来了影响至今的深刻洞见。但他也指出，目前最深的 AI 证明往往只附一份写得很差的 PDF，甚至没有，可能再加一份 Lean 形式化，正确性有超人级别的保证，却看不出思想从哪来。朔尔策举过一个例子：秩为 29 的椭圆曲线构造附带几何解释，而新的秩 30、31 曲线只给了方程，”我们其实什么都没学到”。他还重读了哈代的《一个数学家的辩白》，认为哈代把数学当艺术，动机之一是死后被人记住，与瑟斯顿完全不同。
“理解”作为辩护理由可能适得其反。 巴扎德的关键担忧是：AI 已经解决了一个千禧年难题，而很多同行仍然大大低估了 AI 的进步速度。如果把”理解”当作数学存在的理由，一年后 AI 不仅能证明定理，还能把证明给人类讲清楚时，又该退到哪里？他坦言自己最近被诊断为自闭症，也许这就是他从来不太认同瑟斯顿观点的原因。他当年正是因为朗兰兹领域里充斥着”专家都知道”却没有公开写下的论证而失望，转向了形式化：”你骗不了 Lean”，它不接受以权威或威吓代替证明，”和 Lean 在一起我感到安全”。他又追问”理解”到底指什么：读博时导师理查德·泰勒告诉他三年经费不够读完德利涅的构造，他至今也没读过；今年他讲了 22 小时费马大定理，却对关键的朗兰兹-滕内尔定理细节所知甚少。所以他说自己”在乎的是定理的数量”，承认这是少数派观点。他呼吁 OpenAI 直接把手里的定理全部公开，整理可以以后再做；否则人类可能正在花时间证明一家科技公司早已证出的定理，他认为这近乎审查，并签署了要求公开的公开信。
一个乐观者的理由。 他在 2020 年问过：”如果一个人同时理解全部现代纯数学，他能立刻看得多远？” 现在答案开始显现：机器吸收了互联网上的数学，比如推翻埃尔德什单位距离猜想的证明，正是因为机器同时精通离散几何和类域论，而很少有人两者兼通。他把数学归结为三件事：证明定理、构建理论、提出猜想。目前机器在第一项上表现突出，后两项的证据还很少。对于”你不懂指数增长”的反驳，他的回答是：指数增长不可能永远持续，而数学是无限的，”无限完胜指数”。因此他相信机器会在远超今天的某处遇到新的”自然边界”，到那时再投入资源已不划算；最好的做法是放手让机器跑，看它们停在哪里，再从那里继续出发。结尾他引用希尔伯特的名言：”我们必须知道，我们必将知道！”
HN 评论精华
讨论有 150 多条评论，但需要先说明：大部分评论很快离开了数学本身，转向 AI 对劳动力和阶层的冲击、财富分配、AI 是否失控等泛化话题，真正讨论巴扎德数学观点的评论相对较少。
关于文章本身
- 版主 dang 称赞巴扎德”写得太好了”，越往后越精彩。GPerson 批评巴扎德作为 Lean 的主要推广者立场有偏，把同行说成”在哀悼”不尊重人，而且他不是心理治疗师。dang 回应说文章已经刻意避免冒犯，并点名指出该用户近期多次人身攻击、违反社区规则。GPerson 在另一条评论里直接问巴扎德：等到有一个包含所有数学理论的超大 Lean 数据库时，世界为什么还要资助数学家？Twey 反问：有了相机，为什么还有人付钱给画家？senordevnyc 则认为，数学家到目前为止都没能把这个理由讲清楚。
- slowking2 对数学界只在两种说法里打转感到失望：一种是”做数学是为了理解，所以别用太多 AI”，另一种是”做数学是为了证明定理，AI 来做也行”。他认为两者都是循环论证，给不了外人在乎的理由；更有说服力的是”数学常常会在别处派上用场”，否则数学就只是一种爱好。
- dsubburam 回应巴扎德关于是否”理解”费马大定理证明的追问：就算没有一个人能完整理解，社群把多位专家的理解拼起来，也可以算整体上理解了；如果”理解”本身没有价值，抽象数学的用处就只剩产生新证明，那就成了一种”庞氏结构”。
- piker 质疑数学被”解决”主要靠的是算力和 Lean，而不是 LLM：把模型换成随机数生成器加无限采样，是否也能得到同样结果？azan_ 回答说绝对不行，搜索空间几乎是无限的。sifar 补充说，过去证明过程中走过的弯路常常会开出新方向，把这一步交给 LLM，就会错过这些副产品。
- returningfory2 给不了解背景的人解释：数学正在经历与软件工程类似的技术冲击，但对软件来说只是工具变了，目标还是交付能用的软件；对数学来说，这动摇的是”做数学家意味着什么”。Jaxan 提醒，即使有 Lean 检查，仍然需要数学家确认定理陈述本身是否正确。
- poszlem 提到一个细节：库伯勒-罗斯晚年在采访中说，五个阶段里她自己只经历过愤怒。nicebyte 只回了一句：”听起来像讨价还价阶段。”
跑题后的主线：劳动与资本
- 获赞最多的一条线来自 zaptheimpaler：这类理想主义文章多半出自资深、有保障或富裕的人，对他们来说 AI 带来的变化近乎一个哲学问题；对靠劳动谋生的人来说，这却是生存问题，而且 AI 出现在资本压倒劳动、政府高度腐败的时刻，好处很可能只流向少数人。simianwords 认为多数反 AI 的人其实是觉得 AI 被吹过头，而不是担心被取代；kombookcha 反驳说两者并不矛盾，”一只拿枪的黑猩猩危险，不是因为它枪法好”。bojan 也认为如今的批评大多已经承认 AI 有用，焦点转向了财富集中和环境代价。
- youoy 认为数学界真正的危机是劳动问题：过去数学家用证明换取职位，如今这种”货币”失效了，招聘方该怎么判断一个陌生人？aprilthird2021 不同意，指出学术数学家还要教学，学术数学本来就收入不高，其价值更多是文化和学术上的。
- ramesh31 说自己还没意识到这是哀伤，就已经走到了”抑郁”阶段。ChickeNES 则表示毫不难过，”人类劳动的终结来得越快越好”，随后引出了一串关于财富分配的争论。
- bitwize 说用 AI 写代码像开着作弊码玩《毁灭战士》，能通关但不算真正在玩；他希望将来不靠 AI 编程会像摄影时代的绘画，虽然失去了”容易赚的钱”，但不会消失。doug_durham 认为”手写代码”市场最多只会存在于小众艺术圈。
- 还有几条线完全离题，争论 AI 是否有”意志”、会不会毁灭人类（apsurd、lukan、pixl97 等），以及殖民史能否类比 AI 带来的权力差距（roenxi、graemep）。