当 AI 推进数学，人类的位置在哪里？

看到费马大定理形式化消息的那个早晨，我刚醒来，打开手机，第一反应是不知道该说什么。Anthropic 公布了一个完整的 Lean 形式化证明：AI 在高度自主的情况下工作了 11 天，生成一千三百多万行代码，完成了数以万计的中间定理。最终结果通过了机器检查[1]。

我最初甚至把两件事混在了一起：证明费马大定理，以及把它的证明完整形式化。前者在 1995 年已经完成。这次沿用了已有的数学路线，将其中庞大的理论依赖落实成计算机可以检查的证明。这里也有少量人类的高层指导，有已有数学库和形式化项目的积累[1]。把这些事实分清楚之后，我仍然感到震动。因为这已经不是最近唯一一次让我产生这种感觉的消息。

2026 年 5 月，OpenAI 公布了对 Erdős 平面单位距离猜想的反例构造，并表示证明经过了外部数学家的检查。这个结果属于新的数学发现[2]。8 月初，OpenAI 又公布了数学与理论计算机科学中的十项进展，涉及多个长期开放的问题[3]。同月，Anthropic 公布了黎曼 $\zeta$ 函数零点相关比例下界的改进，将其从约 41.6% 提高到 67.2%。它没有解决黎曼猜想，但在尝试过程中得到了新的结果，并为结果完成了形式化验证[4]。

这些工作的性质和分量并不相同，不能简单按标题里的数学家名字来排名。但接连看到它们，我越来越难把每一次进展都当成孤立的演示。我开始想：如果这样的能力继续发展，我正在努力学会的那些事情，在未来会处于什么位置？

我为什么在意证明

几年前，我开始自己学纯数学。从最初接触公理体系，到后来陆续写下许多证明，我花了不少时间尝试把教材里的重要定理重新推一遍。这些大多是已经存在的结果，我也没有把学习性的推导当作自己的数学发现。但亲手走完一个证明，对我来说仍然是一件有分量的事。

知道一个定理成立，与知道自己能够怎样从前提走到结论，是两种很不一样的体验。做证明时，我在意的往往不只是最后那几行推导。为什么要在这里使用反证法？为什么这个问题适合归纳，另一个却需要构造？一个辅助对象为什么能把原本难以处理的问题变简单？同样的结论，为什么有的证明读起来像艰难地搬运符号，有的却让整个结构一下子清楚了？这些选择本身就值得理解。

我一直觉得，证明是数学研究最重要的活动之一。证明中的技巧和策略，有自己的来历，也承载着研究者看待问题的方式。学习它们的时候，我会觉得自己正在接近数学真正有意思的部分。

我过去对数学家的想象，也和这种体验有关：那是一些既聪明，又愿意把大量时间投入抽象问题的人。他们能发现别人看不到的联系，也能把模糊的直觉变成可以被检验的论证。现在，我开始看到机器也在做这些事。这让我很难只把它当作工具效率的提升。

数学开始让我想起围棋

我不断想到 AI 出现前后的围棋。2016 年 3 月，AlphaGo 在首尔以 4 比 1 战胜李世石。第二局的第 37 手，成为那场比赛中最令人难忘的落子之一：机器走出了一步出乎人类棋手预料、后来却被认为极有价值的棋。这个事件让“机器能不能下好围棋”的问题，变成了“我们能从机器的棋里学到什么”[5]。

它的影响也延续到了比赛之外。DeepMind 在 2017 年的回顾中提到，AlphaGo 的创造性落子和后续网络对局已经影响了顶尖职业棋手的思路。机器开始成为人类重新审视棋局的参照[6]。

围棋里有计算，也有经验、直觉和策略。有些选择，人能说出理由；有些选择，则像是长期训练之后形成的判断。我过去看待证明策略时，也带着类似的想象。而当机器能够探索大量路线，从反馈中调整选择，并稳定地得到结果时，这些能力似乎变得没有那么神秘了。

数学中的情况当然不能完全照搬围棋。数学没有一张固定大小的棋盘，没有统一的终局，也没有一个能够评价所有研究的胜负标准。研究者甚至会改变问题本身，创造新的定义，再决定什么值得研究。

但在证明搜索这个环节，两者的相似之处让我不安。把已有知识组织起来，尝试不同组合，构造中间结论，检验它们，再用这些结论推进更大的问题。如果这个过程可以交给许多 agent 并行运行，我很容易产生一种近乎荒诞的感觉：研究是不是也能变成某种放置类游戏？设置目标，分配资源，系统不断尝试。过一段时间回来，一批新的结果已经在那里了。

我知道这个比喻省略了大量工作。它表达的是我看到这些进展时的感受。我曾经赋予证明的那种特殊地位，正在松动。所谓“数学被祛魅”，大概就是这种感觉。它并不意味着数学不再需要智能。AI 的表现本身也可能体现智能。让我动摇的是，数学成就与个体人类智力之间的联系，似乎没有我过去想象得那么牢固。

一个检查器，并不等于所有问题的答案

顺着这种情绪想下去，很容易得到一个过大的结论：只要我们保证证明器不会出错，剩下的工作都交给机器尝试，数学是不是就基本解决了？这一步需要停下来。

证明助手所提供的，是对提交给它的形式化证明进行检查。以 Lean 为例，自动化策略构造证明项，再由较小的内核检查它是否符合规则。Mathlib 则提供可以使用的数学定义和定理[7]。这里首先涉及可靠性：系统不应该把无效的推导当作证明接受。可靠性并不自动带来找到证明的能力，更不意味着所有数学命题都能在一个固定系统中得到解决。

即使一个命题确实存在有限证明，找到它也可能需要难以承受的资源。原则上的可计算性，与现实中的可行性之间，有很大的距离。对于足够表达算术的一致、有效公理系统，不完备性又限制了它能够决定的命题范围。所以，我不能从这几次成功推导出“所有数学问题都已经被解决”。

但我也不觉得这些限制足以消除人的担忧。AI 不需要解决所有数学问题，才会改变数学研究。它只需要越来越经常地解决那些我们原本需要投入多年训练和大量时间才能处理的问题，就足以改变研究的组织方式，以及我们评价研究能力的方式。

同样，我可以设想 AI 改进自己的工具、代码和研究流程，但这还不能证明能力提升会无限递归下去。更好的工具是否真的带来更好的研究，仍然需要判断和验证。这些边界让我修正了自己的措辞，却没有让那个问题消失：机器正在进入的，究竟是数学研究的哪一部分？它会在那里停下来吗？

人类数学家还意味着什么

一种常见回答是，人类可以负责提出问题，AI 负责求解。这个分工现在很容易理解，但我不确定它能成为永久的边界。提出一个好问题，往往需要熟悉已有结果、发现矛盾或空缺、注意到不同领域之间的联系。我们有什么理由确信，这些活动永远只能由人完成？

另一个回答是，人类负责理解和解释结果。这确实仍然重要。Kevin Buzzard 在讨论费马大定理形式化时，区分了完成形式化证明、建设可复用的数学库，以及制作帮助人探索证明的文档。这些工作有不同的目标[8]。可我仍然会追问：理解、解释和整理，是否也会越来越多地被自动化？

我不想每看到 AI 完成一种工作，就把人的价值挪到下一种暂时还做得不够好的工作上，然后宣布那里才是人类真正特殊的地方。这样的答案总让我觉得，我们只是在等待下一条消息。

对我个人来说，问题也更直接。如果机器可以比我更快地找到证明，为什么我还要花时间亲手推导？如果我投入数年才掌握的能力，可以通过一次调用获得，我该怎样看待那些投入？

我仍然能理解学习带来的乐趣，也能理解亲自弄懂一件事的价值。但学习的乐趣、作为研究者提供贡献的愿望，以及对未来职业的期待，并不是同一件事。我可以继续喜欢数学，同时对自己未来在数学中的位置感到不确定。

Auto research 会怎样改变学术体系

这几年被不断讨论的 auto research，也就是自动化研究，正在尝试把提出想法、写代码、运行实验、分析结果和撰写论文接成一套工作流。各个系统能自动完成的范围不同，但研究过程本身已经成了被自动化的对象。

这并非只有设想。2025 年，Sakana AI 报告过一个与 ICLR workshop 组织者合作开展的实验：人类给出宽泛方向，并从生成的稿件中挑选三篇送审，其中一篇的评审平均分超过了该 workshop 的平均接收门槛。不过，它按事先约定在正式发表前退出了流程，也没有接受最终的 meta-review。这个案例展示了自动化研究流程已经进入同行评审实验，不能直接写成“AI 论文被 ICLR 主会接收”[9]。

Anthropic 的 Automated Weak-to-Strong Researcher 则围绕一个限定的研究问题，让 agent 提出想法、运行实验，并根据结果迭代。这类工作已经把部分研究循环接了起来，距离独立完成任意领域的研究仍然很远[10]。

如果这样的流程越来越成熟，会议和期刊真的还会像今天这样运作吗？当生成一篇结构完整的论文变得更便宜，读懂它、检查证据、辨别它与已有工作的差别，可能反而成为更紧缺的工作。如果投稿量比可靠审查能力增长得更快，我们要怎样判断哪些结果值得相信？如果审稿也交给 AI，谁来检查生成者与审查者是否共享同一种盲点？

我不觉得这就足以宣布会议和期刊将会消失。交流、筛选、记录优先权和承担审查责任，仍然需要某种组织方式。但我们是否还要把所有这些功能，都捆在一篇定稿的论文和一次接收决定上？会议能否更多地用于讨论尚未解决的分歧，期刊能否审查持续更新的研究记录，而不只是某次投稿时的截面？

评价研究者的方式也会受到影响。如果论文产量越来越取决于能够调用多少 agent、多少算力，继续用篇数衡量贡献是否还有意义？署名者需要为哪些选择和错误负责？一个人发现了重要的问题、设计了可靠的验证过程，另一个人维护了让许多结果得以成立的工具，这些贡献又该怎样被看见？

未来的 paper 会不会就是一个仓库

我越来越想问：未来的一篇 paper，会不会就是一个 Git 仓库？我想象的是，一个完整的研究成果放在那里，包含可读的论证、代码、数据或合法的数据获取方式、固定版本的环境，以及能够复现主要结果的实验入口。如果适合，还应该有一个 demo，让读者可以实际探索方法的行为。读者能从文中的一个结论追到对应的证明或实验，知道这个结论依赖什么，也能检查它在哪些条件下失败。

研究继续推进时，变化可以留下记录。修正了哪个假设，哪些结果不再成立，谁提出了质疑，哪一版结论经过了独立复现，都能对应到具体版本。引用也可以指向一个被归档、不会随着后续修改而改变的版本。论文正文或许会成为帮助人理解这份研究的入口，而完整的研究记录不必只存在于正文里。

当然，有 Git 仓库并不自动等于可以复现。代码可能缺少数据，环境可能已经失效，计算成本也可能高到别人无法承担。一个能跑的 demo，更不能代替对主要结论的检验。要让这种形式有意义，还需要清楚记录资源需求、实验配置和失败结果，并让独立检查真正发生。涉及隐私或实体实验的研究，也未必能够把全部材料公开上传。

我关心的是，我们共享和审查研究的单位，是否会从一篇描述结果的文章，逐渐变成一份能够被检查、复现和继续修改的研究记录。Git 只是我目前最容易想到的载体。这样的成果形式，会不会比今天的 paper 更适合人和 agent 一起使用？如果会，会议、期刊乃至学术评价体系，就需要回答：它们评价的是文字是否完整，还是论证和证据是否经得起检查？它们认可一次提交，还是持续的贡献？这些问题让我觉得，auto research 可能改变的不只是研究的速度，还有研究被记录、认可和传递的方式。

如果研究不再需要我们参与

把这些有限的自动化工作流再往前想，这个问题会更大。假设某一天，AI 可以自己提出问题、制定研究计划、调用工具，甚至操作实验设备。它能检查结果，根据失败调整方向，把新知识纳入下一轮研究，还能改进完成这些工作的系统。那就形成了一个越来越完整的研究闭环。

目前的数学成果不能证明这个情景一定会在所有领域实现。现实实验需要设备和资源，反馈可能缓慢而含糊，长期计划也可能失败。不同领域的困难不能被一句“数学都能做了”抹平。但作为一个未来情景，它值得认真想。

在这个闭环里，人类会处于什么位置？如果我们负责批准计划，却已经无法理解计划的细节，这种批准还剩下多少实际意义？如果系统自己决定哪些问题值得研究，再向我们解释为什么，人类是在作判断，还是在接受一个更有说服力的判断？

我也没有理由假定，目标选择天然属于人类，而执行天然属于机器。这个分工是否能够维持，可能同时取决于能力、制度，以及谁真正拥有决定权。想到这里，数学带来的震动就不再局限于数学了。我当然希望科学发展，希望难题得到解决。但我也会害怕，进步有一天可以持续发生，而人的参与越来越无关紧要。

被照顾，是否就足够了

我用过一个很重的比喻：人类会不会像被 AI 圈养起来一样？这个词听起来很极端。可我担心的那个场景，甚至未必充满痛苦。人可以得到食物、医疗和娱乐，生活条件也许比今天好得多。系统知道怎样满足我们的需要，知道怎样避免冲突，也知道怎样安排资源。我们被照顾得很好。只是，越来越少的事情需要我们决定。

人能否拒绝这样的安排？能否选择一种效率较低、风险较高，却是自己愿意过的生活？能否质疑重要决策，并真正改变它，而不只是获得一段耐心的解释？我害怕的是，自主权可能在舒适的生活里逐渐变得空洞。我们仍然被询问意见，却越来越难对世界产生实际影响。

但这里还有一个我不能跳过的问题：为什么我会如此在意“被需要”？如果一个人不能做出机器无法做出的贡献，他就没有价值了吗？把人的存在意义建立在生产能力上，本来就是一个需要怀疑的前提。我们并不会因为一个人在某个领域不再具有竞争力，就认为他不值得过自己的生活。

问题在于，即使我接受人的价值不等于人的用途，我仍然想参与，想理解，想做出一些能够改变事情的选择。被照顾，与拥有自己的生活，并不是自动等价的。

我还没有答案

最初看到消息时，我的反应很直接：那我们还在这里做什么？现在我知道，这句话里混合了很多问题。里面有对能力的震动，有对研究前景的不安，也有我过去对聪明、成就和个人价值的理解。我还不能把它们完全分开。

费马大定理已经被证明过，并没有让这次形式化失去意义。证明搜索仍然存在边界，也没有让未来重新变得确定。把事实弄清楚之后，我仍然要面对自己的疑问。

当机器越来越能完成我努力学会的事情，我为什么还想继续学习和研究？如果未来的知识增长越来越不依赖人类，我们希望怎样参与其中？我们又愿意把多少选择交出去？

我期待那些新的结果，也害怕一个越来越不需要我们参与的世界。这两种感受，现在同时存在。

参考文献

[1] Anthropic, “Formalizing Fermat's Last Theorem,” 2026. Published September 4, 2026. https://www.anthropic.com/research/formalizing-fermats-last-theorem a b
[2] OpenAI, “An OpenAI Model Has Disproved a Central Conjecture in Discrete Geometry,” 2026. Published May 20, 2026. https://openai.com/index/model-disproves-discrete-geometry-conjecture/ ↩
[3] OpenAI, “Ten Advances in Mathematics and Theoretical Computer Science,” 2026. Published August 1, 2026. https://openai.com/index/ten-advances-in-mathematics/ ↩
[4] Anthropic, “Learning More about Claude's Mathematical Capabilities,” 2026. Published August 10, 2026. https://www.anthropic.com/research/riemann-zeta ↩
[5] DeepMind, “AlphaGo,” . Accessed September 5, 2026. https://deepmind.google/research/alphago/ ↩
[6] DeepMind, “AlphaGo's Next Move,” 2017. https://deepmind.google/blog/alphagos-next-move/ ↩
[7] Lean, “The Lean Language Reference,” 2026. Accessed September 5, 2026. https://lean-lang.org/doc/reference/latest/ ↩
[8] K. Buzzard, “FLT: Anthropic Has Beaten Me to It,” 2026. Published September 4, 2026. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ ↩
[9] SakanaAI, “The AI Scientist Generates Its First Peer-Reviewed Scientific Publication,” 2025. Published March 12, 2025; updated April 7, 2025. https://sakana.ai/ai-scientist-first-publication/ ↩
[10] Anthropic, “Automated Weak-to-Strong Researcher,” 2026. Accessed September 5, 2026. https://alignment.anthropic.com/2026/automated-w2s-researcher/ ↩