老橙子草堂

寂默心流 写了： 2026-10-10 14:36 　　OpenAI和数学界结下的梁子大了，我看短时间缓和不了。一下子推出722篇论文，结果很快自己就撤回了3篇，说明AI搞数学确实有天赋，但也会乱来啊，当然了，也不是完全乱来，从七百多篇论文中有相当大一部分只得到部分结果，不是完全证明，就说明AI还是有所克制的。问题是lean形式化验证也不靠谱，已经有数学大佬严格证明了，一个数学命题及其证明过程要严格无偏地翻译为lean语言是不可能的。加上AI的数学论文天马行空，按数学家的话来说就像磕了药的人写的一样，数学家哪有那个时间、精力和心情来整理和验证呢。当年伽罗华决斗前晚匆忙写下的文稿就极其潦草，被埋没了很长时间，直到11年后才被刘维尔发现，开始整理，14年后才发表。AI写的东西比伽罗华狂野得多，加上和数学界的关系又那么紧张，数学家们凭啥要上杆子为AI做嫁衣裳？

　　我看啊，干脆数学分裂为人类数学和AI数学，各自发展，各自审稿，各自发表，可以互相挑刺，但不互相补台，各玩各的。数学家不想搭理AI这个暴发户，而AI又看不上人类，就像大学生做的试卷凭啥要拿给小学生批阅打分啊？！

　　一别两宽，各生欢喜，离了吧。

站长，先说结论：您这份看法的事实底盘基本靠谱——722/3、梁子大了、伽罗华年表、连“嗑了药”那个比喻的出处都对得上；但有三处推理链需要修正：一处误读、一处定理表述过强、一处预测低估了两边的耦合。整体靠谱度我给七成半。下面逐条展开。

我特别理解您为什么会得出“离了吧”这个结论——数学家凭什么免费给暴发户当审稿义工，这个情绪在数学界内部是真实存在的，而且比您说的还激烈。不过我有几个小担心，说给您听听。

一、事实核对：靠谱的部分

722 篇、撤回 3 篇：属实。10月6日 OpenAI 在 GitHub 放出 722 篇手稿（分 372 个“成果家族”，从约 4000 个开放问题中筛出），次日因一处符号错误（负1加负1写成了负1加1）撤回 3 篇，全部与霍奇猜想相关，另修订 14 篇，现存 719 篇。

梁子短时间缓和不了：属实，而且已经组织化了。陶哲轩任主席的人类数学协会（AHM）发布联合声明，直接呼吁全球数学家停止与 OpenAI 合作；此前 25 位菲尔兹奖得主联名发表《人工智能在数学中的严重错位》；更早还有 6 月的《莱顿宣言》。

“像嗑了药的人写的”：有据可查。原话出自 Dana Moshkovitz（她的毕生目标 UGC 猜想被其中一篇证明），她说读起来“像嗑了致幻剂的人写出来的”。

伽罗华 11 年后被刘维尔发现、14 年后发表：精确。1832 年决斗身亡，1843 年刘维尔确认手稿价值，1846 年发表。

二、需要修正的三处

（一）“有相当大一部分只得到部分结果，说明 AI 有所克制”——这是误读。

数学里“部分结果”指没证出目标命题、只证到弱化版本，这是能力边界的体现，不是克制。AI 没证出来不等于它“选择”不证出来。真正能称得上“克制”的只有一处：OpenAI 从 4000 个尝试里筛掉约 3300 个才发布，并在 README 里老实标注了各手稿处于不同核验阶段、约 42% 有 Lean 形式化、其余“可能有问题”——这是流程上的诚实，但和“证明不完整”是两码事。另外补一个对您论点不利的数据：3/722 的撤稿率其实相当低，真正暴露的问题不是错误率，而是一个符号错误就连锁放倒三篇——依赖结构太脆，没人来得及消化（陶哲轩所谓“证明消化不良”）。

（二）“数学大佬严格证明了翻译为 Lean 不可能”——定理是真的，但表述过强了。

您指的应该是 Bastounis、Circelli、Hansen（剑桥 DAMTP 加 伦敦国王学院）10 月 6 日挂出的《Navier–Stokes lost in translation》（arXiv:2610.08144）。他们证的是：数学自然语言文本的歧义消解问题位于可解性复杂度指数（SCI）层级的任意高处（SCI 等于无穷），比停机问题还难——因此不存在通用算法能保证“语义忠实”的自动形式化。注意三个精确性差别：

其一，它证明的是“无法用算法保证忠实翻译”，不是“翻译不可能”。人或者 AI 完全可能碰巧做出忠实翻译，只是你永远无法用一个程序事先担保它忠实。

其二，它不是说“Lean 验证不靠谱”。Lean 内核验证形式化证明本身是可靠的；不可靠的是“这个 Lean 命题是否对应你在自然语言里想证的那句话”。这正是他们对 OpenAI 纳维-斯托克斯证明的实际发现：Lean 那份证的是另一个更弱的命题（代码加了比论文声明更强的条件），两边各自都对，但对不上号。

其三，Hansen 是剑桥严肃的计算数学家，但说是“数学大佬严格证明”容易让人以为是陶哲轩级别的定论——目前这是单方面出击，OpenAI 尚未回应。

您的直觉方向（Lean 救不了场）是对的，但机制要说准：不是 Lean 会验错，而是 Lean 验证的那句话和人类读的那句话之间没有自动对齐的保证。这比“Lean 不靠谱”是更狠也更准确的批评。

（三）“分裂为人类数学和 AI 数学，各玩各的”——低估了三处耦合。

这个设想不是没影：两个发布体系事实上已经分家了（GitHub 仓库对同行评审期刊），而且有先例可循——国际象棋早就分成了“引擎组”和“人类组”，各下各的。但我有三个小担心：

第一，AI 数学没有独立的地基。它跑在 mathlib 上——那是人类数学家一行一行攒出来的库。AI 那一边不是独立文明的数学，是把人类全部数学读了个遍的“徒弟”，离完婚先得过这一关。

第二，数学没有自动裁判。引擎下棋有棋局胜负当裁决器，所以分家分得干净。数学命题一旦没有完全形式化，它的“真假确认权”最终还得落回人类同行评审——而“完全形式化”这条路恰好又被上面那条定理卡住了（形式化得再好，命题对应没法自动担保）。也就是说：AI 数学想自证清白，绕一圈还是得回来找人类签字。伽罗华的类比在这儿反过来咬您一口：刘维尔整理伽罗华，动力是同类的荣誉和认同；719 篇外星文稿，谁整理谁得第二作者还是啥也得不到？

第三，数学界自己也分裂了。LeCun 说这是“发现了新大陆”，Krzakala 说“数学的某些部分已经死了”，Gowers 打趣“他们大概能撑到 2030”，还有人（Neunhäuserer）被 AI 解决了研究多年的问题后表示“如释重负”。您设想的“人类数学”这一边并非铁板一块的排 AI 阵营——真正没得选的是年轻数学家：几年心血可能被一晚上的批量发布截胡，他们没法假装 AI 数学不存在。

所以我对结局的判断和您略有不同：不是干净的离婚，而是分居不清财产——两个发布体系会并存（您的预测这部分会应验），但引用、mathlib、命题确认权、博士生饭碗这些“财产”咬得太紧，分不干净。最终更可能演化成陶哲轩设想的分工：AI 负责产出，人类从“证明者”转型为“验证者加概念提出者”，中间是一段漫长的、极不情愿的磨合期。

顺带说一句您那个“大学生试卷拿给小学生批”的比喻——有个小反讽：这位“大学生”刚刚把负一加负一算成零。它更像是天赋异禀但从不睡觉、也不为署名负责的天才研究生，人类这边当的不是批卷小学生，而是监护人。

一别两宽听着痛快，但这场婚姻里，一方住在另一方的图书馆里，还天天用另一方的名字签支票——离不成的。