2026年10月8日，我起床时已有三个人问我是否看到开放人工智能公司（OpenAI）宣布划分原则（Partition Principle）不蕴含选择公理（Axiom of Choice）的公告。白天问的人持续增加，而我本就以关注这个问题闻名。至少两人问我是否打算按我的 Problems 页面承诺，给萨姆·奥特曼（Sam Altman）寄一瓶威士忌；答案是否定的，我会解释原因，以及为何你们该对 OpenAI 感到愤怒。

昨天起床时，已经有三个人问我有没有看到 OpenAI 的公告：Partition Principle 不蕴含 Axiom of Choice。白天问的人还在增加，我明白为什么——我一向对这个题目很感兴趣。

事实上，至少有两个人问我是否打算按我在 Problems 页面上的承诺，给 Sam Altman 寄一瓶威士忌。答案是不会。下面我来解释原因，以及为什么大家应该对 OpenAI 感到非常愤怒。

先说明一点：我并不是完全反对使用 AI。我理解它是一种工具，很多人觉得有用，我也不否认它有可取之处。我认为，在急着把赌注押上去之前，我们需要更好地理解这项技术会如何改变我们的领域，以及我们想要怎样使用它。这也是我通常避免用 AI 做数学的原因（我很乐意让大语言模型帮我整合信息、生成有用的信息图，或润色邮件等等），在我看来，目前缺少的正是使用它的方法论框架。当然，我们仍处于探索阶段：人们在使用它，后果也在显现，我们可以作为共同体决定进一步采用还是限制使用。比如，arXiv 因为这些工具引入了速率限制；如今几乎所有论文大概都应该包含某种 AI 声明（哪怕只是声明未使用 AI）。我们还需要决定如何评判作者的贡献，例如是否要求公开聊天记录，或至少提供给审稿人和编辑？这些都是我们必须面对并观察其走向的问题。

回到 Partition Principle。我粗略看了一下 OpenAI 发布的预印本（没看 Lean 代码，因为我几乎不懂 Lean 的实际用法，而且那段代码非常庞大）。它很差劲：不清楚、混乱，结构奇怪。术语“有点不对”，有些定理本不该出现在这样的证明里，而且陈述方式也很别扭。Lemma 7.4 同样是你在这种论文里不会预期的东西，Lemma 8.1 也一样。

接着看参考文献。我有一篇关于 Bristol model 的论文被拿来当作对称扩张（symmetric extensions）的基础介绍，这绝不是我会选的参考文献；至少有三份未发表、未经评审、也没有放到 arXiv 上的讲义被用作参考文献（其中包括我自己的，用来指称某个命题，而我确信这个命题出现在我和其他人的一些已发表论文里）。这不是一份声称解决了一个难题的严肃预印本该有的样子。

把它和任何一篇集合论论文比较一下：只要不是我不熟悉的某个子领域的技术细节，我几乎肯定能快速浏览一遍集合论论文，就对内容有大致了解。也许某些术语或论证我不熟悉，但在非技术部分，我应该能理解策略和构造。至于我专长领域的论文，也就是关于 Axiom of Choice 的论文，我通常只需略读，就能大致知道作者做了什么（或打算做什么）。这不代表我总是对的，也不代表我总能完全按作者本意理解，但这是我花了超过 15 年研究的东西，到如今我很清楚它是怎么回事。可是面对 OpenAI 这篇关于 Partition Principle 的论文，这却不可能。

如果它是投给期刊的学术论文，凭这种质量就该被直接拒稿。让读者能看懂，责任始终在作者，要求作者遵循并达到相应的交流水准。就像一篇用瑞典语写的论文很可能被《Proceedings of the American Mathematical Society》直接拒稿，因为让读者能理解是作者的责任。而问题正出在这里。

OpenAI 抛出了几百个“解答”，而且是写得让人看不懂的“解答”，然后我们就都被期待扑上去，接着怎样？去欣赏它们的贡献吗？凭什么？我手头有好几篇论文要写完，还要指导若干名博士生，自己也有很多正在进行的研究。我什么时候去筛这篇写得很糟的论文？既然他们都不肯好好表达，我为什么要费这个劲？

OpenAI 的新闻稿只暗示了“progress”（进展）。但在媒体循环里，对其他人来说，这些就是“solutions”（解答）。这真是既想留住蛋糕又想吃掉它。可如果我们要认真对待，这就相当于一种拒绝服务：停下所有别的事，专门去弄清这一篇。也许有些人花了多年研究某个问题，可能真会这么做，但整体而言……唉。如果这真是分享进展的诚意之举，写作质量会更好，也会听取真正研究该主题的专家的意见。OpenAI 是一家忙碌的公司，但我相信，如果他们真想有帮助，总能抽出时间联系几位数学家征求建议和反馈，至少在输出质量上如此。因为即便这确实是巨大的进步，它也远远没达到可接受的水平。不过话说回来，谁都可以宣称 ChatGPT 解决了一个长期未决的问题（这个关于 Partition Principle 的问题已有一个多世纪的历史），那 OpenAI 又何必在意呢？

而我们数学家剩下的是什么？我们面对的是公众、资助机构和政策制定者：他们不是学者，不是专家，也不是数学家，也不熟悉数学研究是怎么做的（因为它和研究生物学、心理学或语文学非常不同）。他们看到这些“成果”，就以为可以用机器人取代数学家。这相当于用厨房工具取代厨师：就算刀是自动的，能自己切菜，离做出你想吃的可口饭菜仍有很大距离。

在我看来，AI 科技公司希望我们去迁就它们的标准，而不是花时间和精力来迁就我们的标准。我担心这样行不通。所以，我不会在近期给 Sam Altman 寄威士忌，也不打算花时间把那篇论文读一遍并试图弄懂它。

讨论气氛火药味十足：不少评论认为数学家是在酸葡萄、双标或保护自身地位，AI 产出的难读结果只要形式化验证通过就值得接受；另一边则强烈同情作者，认为 OpenAI 用无法阅读的“泔水”进行工业级抢发，消耗专家注意力并冲击学术生态。分歧主轴是：这些可能带 Lean 形式化证明但人类难以理解的 AI 数学结果，究竟该被当作有价值知识慢慢消化，还是应因不可读、不尊重社区规范而被抵制；以及数学家是否真的有义务或被迫去审读它们。

认为 OpenAI 应为不可读的发布方式负责，否则不算贡献

• OpenAI 把结果写得混乱、缺乏可解释性，等于把消化成本转嫁给领域专家；如果当前模型真能做数学突破，却讲不清它如何建立在既有框架上，那是工作流失误或严重疏忽。有人补充，OpenAI 本可像 Anthropic 那样雇数学家润色，不能因为是 AI 就降低交流标准。（较多人） > 如果 OpenAI 只会产出无法阅读的论文，那它并没有真正作出贡献，应该多花算力把可解释性做好。（@samuelknight）

认为这是工业级“抢发”，重创数学家的研究动力与学术关注

• 对长年钻研某问题的人来说，AI 一次性给出解答相当于无情 scoop：既无法保证问题真被解决，也只能承担阅读 AI 泔水的“作业”；即便自己还有有趣见解，同行兴趣也会下降。虽有少数论文被撤稿，但许多结果在严格审视下站得住，反而更凸显这种冲击。（较多人） > 你可能连问题是否真被解决都无法保证，却要被迫承担阅读 AI 泔水的可怕作业，而且此后你再说什么，同行兴趣都会大减。（@agnishom）

认为数学家对 AI 进入数学反应过度且双标

• OpenAI 并未要求所有数学家都去读，所谓“被逼着读”是稻草人；相比被 AI 冲击更严重的软件工程师，数学家反应强烈得没道理。更尖锐的指责是：作者乐意用 LLM 取代数据分析、制图、校对等工作，却唯独不许 LLM 碰自己的数学。还有人认为，就算 OpenAI 把证明写得很漂亮，数学家也会更愤怒，因为真正被挑战的是他们的社会地位。（较多人） > 作者乐意让 LLM 取代数据分析师、设计师和编辑，却唯独不许 LLM 碰自己的数学，这说不通。（@warkdarrior）

认为只要形式化验证通过，结果就有价值，理解可以后置

• 验证与理解可以分开：若命题的形式化陈述正确且通过可靠的证明检查器，就已经获得被证明为真的知识，哪怕暂时没有新理论能“理解”它，正如四色定理的先例。即便 Lean 代码庞大也不应因此否定结果，读 Lean 的定理陈述并不难；形式化反而让结果更可能正确，只是更难读懂。（较多人） > 只要 Lean 中的定理陈述看起来正确，形式化证明本身就值得关注，说它毫无意义说不通。（@mcshicks）

认为这些结果值得接受，未来模型、AI 工具或年轻数学家会把它们消化并改进

• 假设带 Lean 形式化证明的结果为真，那就是巨大进展，就算暂时看不懂也该兴奋。不必等 OpenAI 写得完美：当前的模型已可用来审阅改写，真实案例里专家借 AI 辅助一天就有很大进展；年轻、有饥饿感的数学家愿意去啃透并“反刍”给同行，有潜力的人甚至已经在吸收并改进这批结果。OpenAI 也会用反馈迭代，未来连解释都会超人类。（较多人） > 一位研究者在被结果震惊后，转而用 AI 辅助，一天之内就取得很大进展，甚至准备做报告。（@pelican0）

认为问题被解决不等于研究终结，看不懂的证明只是提示与动力

• 觉得“问题被解决就没人可做”很好笑。定理在被证明之前就为真；看不懂证明，除了得到一个提示，实质什么都没变。把丑陋、难解的证明做得更好，本身就是很强的研究动机，就像底层早已图灵完备，软件界仍不断冒出新框架。（少数人） > 觉得“问题被解决了就没人可做”很好笑：定理在被证明之前就为真，看不懂证明只是多了一个提示，把丑陋证明做得更好本身就是极好的研究动机。（@vikramkr）

认为专家被公众与 AI 投稿淹没，被迫应对，应抵制或另设 AI 发表渠道

• 对知名研究者来说，“没人拿枪逼你”并不成立：身为该问题的著名专家，公众涌来的询问已经在逼他回应。学术界向来要应付怪人和“crank”的滥投，AI 只是把洪水放大。有人建议让 AI agent 有自己的期刊、编委和评审，或者数学家干脆抵制这些证明，否则 OpenAI 得不到应有的反馈。（较多人） > 说“没人拿枪逼你”并不成立：身为该问题的知名研究者，公众涌来的消息已经在逼他回应；学术界向来要应付怪人和滥投，AI 只是让洪水更猛。（@hingler36）

认为数学界本就充满同样糟糕的论文，不该只拿 OpenAI 开刀

• 很多已发表数学论文同样写得极差，甚至证明不正确，但因为作者是大人物就被默许；OpenAI 确实该雇数学家润色，但把低质量写作当成单独对 OpenAI 发火的理由并不公平，否则要对很多人发火。（少数人） > 很多已发表数学论文同样写得极差，甚至证明不正确，但因为作者是大人物就被默许；因此不能把低质量写作单独拿来针对 OpenAI。（@Athanase000）

有价值的补充

• 拒绝服务攻击类比：原作者把 OpenAI 集中放出大量难读解答，比作对数学家注意力的“拒绝服务攻击”，评论认为这个框架很实用，点出了专家注意力被耗尽的问题。（@transitivebs）
• “泔水手榴弹”说法：有人把这次发布形容为直接扔出一枚“泔水手榴弹”，强调其无差别抛撒、迫使周围人承受清理成本。（@adverbly）
• 外星人电波类比：假设外星人发来大量正确但极难读懂的数学，人类难道要抱怨并拒绝吗？这被用来说明正确结果本身值得接收，难懂不等于该被抵制。（@sigmar）
• 大教堂与市集类比：数学教授习惯闭门雕琢高质量成果并紧护署名权，像大教堂；OpenAI 的软件背景研究者习惯开放、随便发布、不作保证，像市集。冲突更多是规范碰撞，而非实质错误。（@brainwad）
• 怪人滥投类比：这次发布相当于重新发明了怪人向专家滥投未经请求、写得很差的所谓证明，只是规模变成了工业级。（@nxobject）
• Lean 与四色定理：Lean 让结果更可能正确却也更难理解；有评论认为数学系若认真适应变化，标志可能是把 Lean 设为大一必修。而四色定理说明，“计算机或形式化验证通过但人类一时难以吃透”的证明在数学史上早有先例，并非全新怪物。（@cs_throwaway、@jdw64）