就在 Claude 用 Lean 完成费马大定理证明形式化的同一周，一篇题为《球面哈德维格定理》的论文出现。球面哈德维格猜想自 1974 年左右悬而未决，描述的是积分几何中虽冷门但重要的一件工具。湖南大学 Wang 与 Wu 的新预印本似乎借助人工智能证明了该猜想，并在文末免责声明中写道，OpenAI Codex 被用来协助打磨证明细节、定位漏洞与需澄清处、组织排版并润色英文。

在 Claude 于 Lean 中完成费马最后定理证明形式化的同一周，我的邮箱里收到了一篇题为《球面 Hadwiger 定理》的预印本。球面 Hadwiger 猜想自 1974 年左右悬而未决，是积分几何中冷门却重要的机制。这篇由湖南大学 Wang 与 Wu 撰写的预印本显然借助 AI 辅助证明了该猜想。文末免责声明写道：

在准备本手稿期间，使用了 OpenAI Codex 来辅助开发证明细节、识别漏洞与需澄清之处、组织与排版手稿，以及编辑英文。作者审核并验证了所有 AI 辅助的数学内容，提出修改建议，做出所有最终数学与编辑决定，并为手稿承担全部责任。

这段声明意味着 Codex 可能完成了原本需要研究级数学家的工作：开发证明细节、找补漏洞，甚至撰写论文。而且成稿非常精炼易读（对该领域研究者而言）。

我尚未完全验证证明，只用 Claude Fable 过了一遍，感觉靠谱，但完全消化需更多精力。这并非批评 Wang 与 Wu，论文看起来很棒，也遵循了 Leiden Declaration 的 AI 使用原则。

切身的里程碑

对我而言，球面 Hadwiger 定理的证明切身相关。我读研时尝试证明过，今年初还用 AI 半心半意试过一次。它不是抢头条的公式，却也没能幸免。

我本不该惊讶。GPT-4 发布时，OpenAI 有份报告谈 LLM 对劳动力的潜在冲击。数学家工作受 AI 干扰的暴露度在所有建模类别中最高；白皮书估计，跨三种劳工模型，数学家 100% 的工作都暴露于 LLM 之下，高于作家、翻译、艺术家和平面设计师。唯一区别是数学家感受到痛感稍晚。

若带点傲慢，可以说数学领域 LLM 主导来得晚是因为研究级数学最难。但我怀疑，延迟更多因为研究数学经济价值更小、训练数据更少。

想想古典音乐。社会并不像支持流行音乐家那样支持古典音乐家。古典音乐被制度化，作为遗产送进音乐学院。一小部分人认定保留演奏能力值得，遂投下少量资本：培养年轻人，在大城市雇最好的演奏家。

这模式能套用数学家吗？容易想象：欧几里得时代，数学主要是少数有缘人的智力追求。数学音乐学院能帮助数学繁荣，即便创造新结果不再难，理解和传达其意义仍难。

但纯数学早已在音乐学院里了，也就是学术界。大学之外，纯数学家职位稀少，成果只有少数人懂。既然硬结果很快都将由计算机证出，这还重要吗？

底线

值得支持人们继续从事如今被称为“研究数学”的文化事业。数学尤其纯数学，始终是沟通那些帮我们更深理解现实的故事。通过简化与抽象，我们看见隐藏结构：平行线不相交，球面各向同性，素数无穷。

但支持数学家的现行系统，如同诸多创意领域，亟需剧变以应对 AI 新现实。激励结构与 AI 带来的东西格格不入。这些工具让人更难判断复杂论证是否正确，更别提谁该得经费、终身教职与名望。摆在我们面前的选择是：当人类智力劳动根本比不过计算机，我们如何让人继续重要？当智能只受限于硅与电，我们是否仍愿支持一个有数学家的文化？我由衷希望如此。

讨论焦点在于数学是否会如古典音乐般沦为机构供养的小众活动，多数意见认为类比牵强且数学家角色将转型而非消失，少数声音宣称AI已能代管数学发现与阅读。

认为原文章将数学类比古典音乐是牵强且前提错误

• 数学并非仅关乎娱乐，且纯数学早已处于学院中，“进入音乐学院”之问本身奇怪；古典音乐实际获政府拨款等支持，并非被社会抛弃。（认可度：较多人）
• 需要引用时，只用一句中文意译： > 数学不只是娱乐，这个类比显得生硬（@pfdietz）

认为数学家的角色会因AI转变但绝不会消失

• 总需有人决定计算资源投向、哪些定理值得投资、提出公理基础并验证AI产出；人类理解与沟通是数学核心，无人需要未被人类验证的数学。（认可度：高赞）
• 需要引用时，只用一句中文意译： > 没人愿看机器人互弈，也没人需要未经理人类验证的数学，人类理解才是数学要害（@chr15m）

认为AI将加速数学进展甚至自主完成发现与验证

• 模型已能生成并审阅证明，节奏快过人脑；借助AI普通人也能构思并用数学支撑发明，相当于把物理说出口即成形。（认可度：少数人）
• 需要引用时，只用一句中文意译： > 正如预言，数学将由模型生成与阅读，进展不再受人类脑力束缚（@a2ff6eeb0）

认为社会对各领域艺术工作者的支持模式相似且古典并未断粮

• 无论流行或古典音乐家皆靠教学、婚庆演出等兼职谋生，所谓音乐学院系统供养说不通；若把社会视作政府，其对古典的资助可能多于流行。（认可度：较多人）
• 需要引用时，只用一句中文意译： > 若将社会具象为政府，它通过拨款对交响乐等的支持恐怕多于流行音乐（@rayiner）

认为学科危机本质是“过程还是结果”的争论

• 反AI艺术情绪多源于认定艺术是过程非结果；数学研究需求不减甚至加速，但方法在变；即便机器人表现更优，人们仍愿为真人表演付费。（认可度：较多人）
• 需要引用时，只用一句中文意译： > 去酒吧人们宁愿多花钱请真人弹唱，也不要更好听的点唱机（@pianopatrick）

认为当前AI连基本事实都不可靠，不能轻信

• 有用户调侃AI连自行车螺栓尺寸都搞错，却正被指望推送数学进音乐学院，反映对底层事实可靠性的怀疑与社区幽默情绪。（认可度：少数人/玩笑）
• 需要引用时，只用一句中文意译： > 人工智能连8毫米和10毫米扳手都分不清，竟忙着把数学推向音乐学院（@kazinator）

有价值的补充

• 未来数学家或可提出不同公理基础（如 ZF、ZF+C 等），再用计算机推演后果（@kdavis）
• 金属加工职业并未因工艺变革而消亡，只是工作形态不同且从业减少，数学亦将如此（@gpm）
• 多数数学发现源于工程需求而非闲余智力追求，毕达哥拉斯式发现实为分账驱动（@whateverboat）
• AI数学成果多出人类设定问题，若无人提问赏识，资本不会持续投入（@nxpnsv）