文章目录罗博深真正想保住的不是一份职业当证明越来越便宜理解会不会更贵AI 已经走到哪一步哪些数学工作会先被自动化哪些工作反而会升值数学教育、论文和经费都要改人类数学家的角色不会原样保留参考资料2026 年 9 月 19 日陶哲轩的个人博客刊出了一篇标题相当直接的文章《Why Do We Need Human Mathematicians Anymore?》中文可以译作《我们为什么还需要人类数学家》。文章很快被转到 Hacker News。9 月 20 日保存的讨论快照显示帖子获得了 248 分和 264 条评论到 9 月 26 日再次查看时页面已经显示 292 分、377 条评论。数字还会继续变化但讨论为何升温并不难理解这一次被摆上自动化天平的不是客服、翻译或程序员而是常被视为纯粹智力象征的数学家。不过先要澄清一个容易被标题掩盖的事实。文章发布在陶哲轩的博客上却不是陶哲轩本人撰写。页面开头明确说明这是数学家罗博深Po-Shen Loh的客座文章由他的个人博客转载而来。陶哲轩提供了平台也参与了这场更大的讨论但文中的“人类繁荣”公理、AI 控制点等具体论证首先属于罗博深。把它简写成“陶哲轩认为”会让事件变得更醒目也会让事实失真。这项区分并没有削弱问题的分量。恰恰相反陶哲轩的博客在短时间内连续刊登不同数学家对 AI 的看法说明数学界已经不再只问“模型能不能解题”。现在的问题是当 AI 能生成证明、搜索猜想甚至处理过去被认为需要顶尖研究者才能推进的问题时数学研究究竟在生产什么如果答案只是“正确结论”人类数学家的处境确实不太乐观。如果数学还包括理解、选择、解释与责任那么变化的可能不是这个职业是否存在而是我们怎样评价它。罗博深真正想保住的不是一份职业罗博深的论证从一个价值判断开始人类应当帮助人类繁荣。他把这句话称为一条“公理”。这听起来近乎常识却承担了整篇文章最重要的工作。如果不先接受这个价值前提那么社会为什么要花钱维持一个由人类组成的数学研究共同体假设一套 AI 系统可以稳定地产生正确、有用且经过形式验证的数学结果公众可能并不在意证明是谁写的。新材料能否被发明飞行器能否更安全天气模型能否更准确似乎都比作者是人还是机器重要。单凭“数学家喜欢做数学”显然不足以成为公共资助的理由。罗博深给出的回答不是证明人类永远比 AI 更聪明。他承认未来系统可能以远高于人的速度积累定理、整理概念并寻找应用。人类也可能成为效率较低的一环。他真正坚持的是研究方向的取舍不能只由能力最强的系统自动决定。研究昂贵未知问题又近乎无穷因此总要有人决定先探索什么、承担什么风险、把资源交给谁以及成果最终服务什么目标。要做这种决定人不能只坐在控制室里看仪表盘。一个失去专业能力的监督者很难判断模型是不是偏离了问题也看不出一份形式正确的结果是否回答了真正值得回答的问题。因此人类若想保有对数学研究的方向权就必须保有一批仍在前沿工作的数学家。研究实践不是给监督者准备的装饰性履历而是他们能够监督的前提。这套论证的优点是没有把“人类不可替代”建立在某项暂时领先的能力上。历史已经多次证明凡是可以清楚列成能力清单的护城河都可能被技术跨过。计算速度、符号变形、定理检索、形式化检查已经先后从人的专长变成机器擅长的工作。罗博深选择了另一个支点谁有权决定目标谁就需要足够的知识承担决定的后果。它也有明显的争议。HN 用户 auggierose 追问即便“帮助人类繁荣”成立为什么每一个领域都必须由人来掌舵如果 AI 管理“世界数学部”更有利于人类把控制权留给人是否反而是一种执念围绕“物种主义”的争论也由此出现。这个词很抓眼球但容易把更实际的问题挤到一边我们还没有一套公认的方法把“人类繁荣”翻译成数学研究的具体优先级更不能假定所有人、机构和 AI 公司对它有相同理解。这里引用的只是几条讨论意见并不代表数学界共识。所以罗博深给出的不是定理而是一项政治与伦理主张。它不能靠 Lean 检查也没有唯一答案。可这正说明数学的未来并不只是技术问题。当证明越来越便宜理解会不会更贵围绕 AI 与数学的讨论经常卡在“过程还是结果”。一种常见说法是数学家真正重视的并非答案而是抵达答案的路径。一份证明的价值在于它告诉我们为什么结论成立揭示哪些概念彼此相连还可能在途中留下可复用的方法。HN 用户 xanderlewis 把数学活动粗略分成三个步骤观察某种现象把它形式化为可操作的结构再从假设中推出新的结论。公众容易看见第三步因为它最像考试也最容易被写成输入与输出。前两个步骤却决定了问题从哪里来、现实中的什么东西值得抽象、哪些条件应该保留。若只比较最后一步人类当然显得缓慢。评论者 bayindirh 用了更形象的说法科学探索的路径不是从 A 到 B 的直线而是一棵树。人在寻找某条证明时会注意到岔路、失败和意外类比。原问题没有解决旁边的想法却可能进入另一个领域。一套以尽快完成既定目标为优化方向的系统未必会保存这些岔路更不一定知道哪条岔路对人类有意义。但这类辩护存在一个隐含前提未来的 AI 无法表现出类似的创造力。HN 用户 Spacecosmonaut 直接指出数学家常说“过程比结果重要”并不能由此推出只有人能创造有价值的过程。AI 完全可能在搜索中提出新概念、保存旁支结果再用人类可读的方式解释。今天的局限不是永久的本体差异。这条反驳很重要因为它迫使我们把“人类价值”说得更具体。不能因为某个模型目前不善于选题就宣布选题永远属于人也不能因为机器生成的证明难读就认定机器永远无法解释。比较可靠的结论是证明、理解和选择是不同的产品自动化速度也不会完全同步。哪一项先成熟数学共同体的评价体系就会先在哪一处承压。2026 年 9 月 18 日也就是罗博深文章发布前一天陶哲轩博客还刊登了 3Blue1Brown 创作者 Grant Sanderson 的客座文章。他提出如果数学的目标不止是证明而是增进人的理解那么学界就应认真奖励“有动机的解释”而不是在 AI 大量生成证明之后才临时宣布解释更重要。这是一个略显尴尬却必要的提醒如果过去的职位、奖项和论文制度主要奖励“谁先证明”那么今天突然用“数学不只是证明”保卫人的地位听上去很像移动球门。要证明解释真的重要最有说服力的办法不是写宣言而是改变评价方式。AI 已经走到哪一步讨论不能只停留在哲学层面。AI 数学能力在过去几年里有了可测量的进展而且 2026 年的事件已经越过“会做竞赛题”这条线。OpenAI 在 9 月 8 日发布的说明中称其内部系统给出了 Navier-Stokes 千禧年难题相关陈述的解析证明和 Lean 形式化版本。证明展示了带光滑外力的三维不可压缩流体可以在有限时间内形成奇点。OpenAI 表示这对应官方问题表述中的 C 和 D并明确说不打算申领奖金。更值得关注的是它公开的生产方式。官方说明称项目动用了约一万个并发智能体运行约 88 小时与 Navier-Stokes 结果有关的智能体交换了约 270 万条消息生成约 1300 亿个输出 token。随后GPT-6 Astra 又用了 17 小时完成 Lean 形式化与验证。团队还让不同智能体群探索不同路线再用 Codex 汇总有用线索并交叉传播。这些数字来自 OpenAI 自己的披露不能替代独立复核却足以说明一种新的研究形态正在成形。AI 的优势不只是一名“电子数学家”推理更快而是可以把成千上万条搜索路线同时展开再用形式化系统筛除部分错误。这更像一个算力充足、昼夜不停的研究组织。它的边界也写在同一份说明里。问题由人选择系统被告知哪些方向最值得投入来自不同智能体的线索需要被组织最终结果还要转化为数学共同体能审查的论文与形式证明。大规模并行也带来新的评价难题如果只公布成功案例不公布尝试了多少问题、失败路线消耗了多少资源就很难计算系统真实的成功率和研究效率。HN 上关于“100 个智能体年”和“人类研究年”的争论之所以没有定论部分原因正是机器搜索与人类研究留下的产物并不相同。人类失败的路线可能沉淀为论文、方法和学生训练机器失败的数百万条消息则可能永远不会公开。更早的 AlphaProof 与 AlphaGeometry 2 提供了另一个参照。Google DeepMind 在 2024 年报告两套系统合计解决了当年国际数学奥林匹克竞赛六道题中的四道达到银牌分数线。AlphaProof 负责形式化的代数与数论题AlphaGeometry 2 处理几何题。不过题目先由人工转成形式语言除一道题在几分钟内完成外其余题目最多求解了三天人类选手参加正式比赛时只有两个 4.5 小时的场次。这不是一次与人类考生同条件的参赛。它仍是清晰的技术进展却发生在边界明确的竞赛环境中题目已经给出正确性标准清楚验证方式也相对可定义。从竞赛解题到开放研究中间至少隔着问题发现、概念形成、文献判断、资源分配和结果解释。OpenAI 的新案例缩短了这段距离却没有让它消失。把 AlphaProof 说成“只会做题”会低估技术把它说成“已经会做完整的数学研究”则夸大了结论。哪些数学工作会先被自动化“数学家会不会被取代”太宽拆成具体工作更容易回答。以下几类任务最可能先进入常态化自动化。第一类是文献检索与关系整理。研究者面对的论文数量远超个人阅读能力。AI 可以寻找相似命题、追踪符号差异、整理某个引理在不同文献中的版本并为新问题建立候选知识图谱。这项工作仍需要核对原文但机器已经能显著压缩搜索时间。第二类是候选引理与证明路线搜索。给定清晰目标后系统可以并行尝试变换、构造反例、调用数值实验或者把问题拆成多个子目标。大量路线会失败机器可以并行承担这些尝试减少研究者逐条试错的时间总体成本是否更低仍取决于算力消耗和筛选效率。第三类是符号推导和重复计算。计算机代数系统早已改变应用数学家的工作。HN 用户 qubex 提到自己不擅长心算和手工推导还有阅读障碍却能借助 Derive、Matlab 与 Mathematica 探索直觉。他把工具比作天文学中的望远镜过去敏锐视力可能是观测的门槛仪器出现后研究者的价值转向提出问题和理解信号。AI 把这条旧路线又向前推了一步。第四类是形式化与验证。自然语言证明中常有“显然”“类似可得”这类跳步。Lean 等证明助手要求每一步满足形式规则能发现人类审稿容易漏掉的空隙。当 AI 能协助把论文转成形式语言形式验证的成本会下降。需要注意的是形式系统验证的是结论能否从给定公理和定义推出不会替人判断定义是否贴合原问题也不会自动证明研究目标值得追求。第五类是多路线并行探索。这可能是最具破坏力的一项。一个人一次只能认真追踪少数思路而智能体群可以把搜索空间铺开。哪怕单个智能体的“品味”一般只要并行规模足够大、验证器足够可靠系统也可能在结果生产上超过顶尖团队。把这些工作交给 AI不等于数学家变得无事可做。它意味着以手算速度、记忆量和局部推导熟练度建立的优势会贬值。电子计算器没有消灭数学却减少了课堂对某些重复计算的训练需求。AI 同样会迫使研究者解释除了一步步把证明写出来你还能为问题带来什么哪些工作反而会升值最先升值的是选题。可验证的定理有无数个值得投入时间的定理很少。一个问题是否连接重要现象是否可能产生新方法是否在当前知识条件下可推进背后都包含判断。AI 可以给出候选项但最终的优先级还涉及机会成本和公共价值。其次是概念创造。优秀的数学工作不只是把旧符号推得更远有时会发明一种新的表述让原本分散的事实突然显得属于同一个结构。未来 AI 也可能做到这一点但共同体仍需要判断新概念是压缩了知识还是只给复杂输出换了名字。解释能力也会变贵。形式正确的证明若只有少数机器能处理数学知识就可能变成一个巨大的黑箱数据库。人类需要知道关键想法是什么、为什么这种方法有效、条件改变后哪里会失效。解释不是把长证明“翻译得简单一点”而是重新组织知识使其他人能够迁移和使用。审核与追责会成为独立工作。AI 生成速度越快待审结果越多。形式证明能过滤逻辑错误却过滤不了错误建模、数据污染、隐藏假设和不当研究目标。论文作者、期刊和资助方必须回答哪些步骤由 AI 完成使用了什么工具和计算资源人类检查到了什么程度。否则“通过验证”可能成为新的权威标签却没人对验证范围负责。跨领域建模同样会更重要。现实问题很少以整洁定理的形式出现。把流体、疾病传播、供应链或能源系统抽象成数学对象需要与领域专家反复确认哪些细节可以忽略。模型求解可以高度自动化错误的问题定义却会更快地产生错误答案。最后是教学和共同体建设。人不能在完全停止实践后仍长期保持前沿判断力。若下一代学生从入门阶段就把推理全部外包未来可能缺少能够检查 AI 的研究者。保留人的专业能力并不意味着禁止工具而是要设计新的训练学生可以使用 AI但必须能质疑其假设、重建关键步骤、比较不同证明的解释力并清楚标注自己完成了什么。数学教育、论文和经费都要改如果证明生产成本继续下降最先需要调整的是数学教育。传统课程常用大量同型题训练符号熟练度因为这种能力过去既是理解基础也是考试中方便测量的代理指标。AI 出现后机械推导仍需掌握到足以检查工具的程度却不该继续占据主要评价空间。考试可以增加问题建模、错误诊断和解释比较。给学生两份都能通过形式检查的证明让他们判断哪一份更有启发性给出一个 AI 建立的模型让他们找出被忽略的现实条件要求学生说明为什么选择某条路线而不只是提交终点。重点不是把考试改成“和 AI 聊天”而是测量工具难以替学生承担的判断。论文评价也要摆脱只看首个正确结果的惯性。如果一个 AI 系统率先证明了猜想人类研究者随后给出更短的证明、解释关键机制或把方法推广到新的领域这些贡献不应被视为“二次加工”。Grant Sanderson 所说的“有动机的解释”可以成为正式成果类型但需要清楚标准解释带来了什么新理解哪些人能够因此解决以前解决不了的问题是否产生了可复用的概念。出版规范需要记录 AI 的参与方式。简单写一句“使用了 AI”没有多少信息。更有用的披露包括模型或系统版本、任务范围、是否访问外部文献、候选结果如何筛选、形式验证覆盖到哪里、人类复核了哪些关键步骤以及大致计算成本。这样做既是为了学术诚信也是为了让后来者能够比较方法而不是只能相信一次漂亮演示。科研经费分配会遇到更尖锐的问题。大规模智能体搜索需要算力算力集中在少数公司和机构手中。如果数学成果越来越依赖昂贵计算谁能选择目标、谁能看到失败记录、谁能复现结果就会影响整个领域的议程。公共资助不能只购买最终答案还应支持开放数据、可审计日志、形式化基础设施以及不依附单一公司的研究者共同体。这也解释了为什么“AI 能不能做数学”已经不是最重要的问题。它当然能做而且能做的范围正在迅速扩大。真正缺少答案的是AI 产出的数学如何进入公共知识谁来验证它谁来解释它失败成本由谁承担研究方向又由谁决定。人类数学家的角色不会原样保留面对职业冲击人们很容易落入两个舒服的结论。一个是“AI 只是工具人类永远不可替代”另一个是“既然 AI 能证明定理数学家很快就没用了”。前者低估了自动化能力后者把数学缩成了答案工厂。更可能发生的变化是数学家的角色重新组合。过去一名研究者可能同时负责找问题、查文献、做推导、写证明、解释结果和说服同行。未来其中许多环节会由不同模型、证明助手与智能体群完成。人的工作更接近提出问题、设置约束、组织探索、审查证据并为研究选择负责。这不保证数学家数量一定增加也不保证现有职位和经费安然无恙。重复性较强、评价目标清楚的工作可能收缩年轻研究者依靠“小问题”练习并建立声誉的路径也可能被挤压。若学界只在口头上强调理解却继续按证明数量和抢先发表分配机会AI 带来的不会是更高层次的数学共同体而是更快的成果竞赛。qubex 借助计算机代数系统工作的经历给出了另一种可能。工具没有让他的数学直觉失去价值反而绕过了手工计算与阅读障碍让他能够进入过去难以参与的探索。AI 也可能降低数学研究的技术门槛使更多人能测试想法、建立模型和接触形式证明。门槛下降会带来噪声也会带来原本被排除的人。“还需要人类数学家吗”不是一道等待 AI 给出 yes 或 no 的题而是一份写给数学共同体的制度设计作业。未来最稀缺的或许不再是能最快写出证明的人而是知道该证明什么、能看懂机器为何得出这个结果并愿意对下一步往哪里走负责的人。参考资料Po-Shen Loh 客座文章Why Do We Need Human Mathematicians Anymore?Terry Tao 博客2026-09-19。Hacker News 讨论Why do we need human mathematicians anymore?页面数据于 2026-09-26 核验。OpenAIOn the Navier-Stokes Millennium Prize Problem2026-09-08。文中有关智能体规模、消息数量、token 与 Lean 验证时间的数据均为 OpenAI 自述。Google DeepMindAI achieves silver-medal standard solving International Mathematical Olympiad problems2024-07-25后续页面注明 2025 年发布 AlphaProof 方法论文。Grant Sanderson 客座文章If math is more than proof, we need to better celebrate the rest of itTerry Tao 博客2026-09-18。