AI人工智能时代的数学家们——杰里米·阿维加德

AI人工智能能够以形式化和非形式化的方式证明数学领域的研究级定理。当前全球交互式定理证明（Lean）与形式化数学领域的核心领军人物之一、卡内基梅隆大学教授杰里米·阿维加德（Jeremy Avigad）呼吁数学家们紧跟该技术的发展步伐，思考其对数学研究实践的颠覆性影响，并以恰当的方式应对当下面临的挑战与机遇。

杰里米·阿维加德（Jeremy Avigad）卡内基梅隆大学教授

作者：杰里米·阿维加德（Jeremy Avigad，卡内基梅隆大学教授）2026-3-7

译者：zzllrr小乐（数学科普公众号）2026-4-1

致谢

感谢约翰·科梅林（Johan Commelin）、西德哈斯·哈里哈兰（Sidharth Hariharan）、布莱娜·克拉（Bryna Kra）、埃米莉·里尔（Emily Riehl）与阿克沙伊·文卡特什（Akshay Venkatesh）提供的意见、修正建议与研究思路。

1 研究背景

过去一年，美国国家科学基金会（NSF）的发展步履维艰，但即便其下属所有研究所的预算均被削减，该基金会仍在去年秋季成功成立了数学计算机辅助推理研究所（ICARM）。该研究所的使命是支持数学领域新推理技术的应用，其中多项技术均涉及神经人工智能与符号人工智能。作为研究所所长，我曾以《AI人工智能时代的数学》为题发表过多版演讲，梳理了各类新兴技术，包括形式化与证明助手、符号人工智能与自动推理，以及机器学习与神经网络。这些技术虽各有不同，却存在有趣的交叉与互动。

迄今为止，形式化方法的早期实践者为数学形式化库Mathlib做出了贡献，多个合作项目已借助该库验证了当代数学研究成果，部分成果的验证甚至早于常规同行评审流程，或是在未开展同行评审的情况下完成。SAT求解器等自动推理工具解决了组合数学、代数学、数论与离散几何领域的多个公开问题；机器学习技术被用于挖掘计算数据中的模式及数据间的关联，助力新研究成果的发现，且这些成果均已通过传统证明方式得到验证，该技术还被用于寻找具有研究价值的组合对象，包括某些猜想的反例；神经网络则被用于求解偏微分方程、识别具有研究意义的现象，以及寻找能催生此类现象的参数设置。尽管这些技术目前仍属于小众领域，且仅有为数不多的显著成果，但相关进展足以表明，它们必将对数学学科产生重大影响。

神经网络将机器学习与符号方法相结合，被应用于数学定理的证明工作。这一应用有时表现为利用语言模型和智能主体系统撰写非形式化的数学论证过程，有时则是借助其构建形式化证明，而这些证明的正确性会由Lean等证明检查器进行验证。许多系统会在两种推理层面交替进行，既借鉴传统数学文献中的洞见，又依托形式化检查器提供的强正确性验证信号。该领域近期的发展尤为显著。我在各类演讲中对这些技术的整体态度始终较为乐观：新兴技术能够助力我们更好地开展数学研究，完成以往无法实现的研究工作。它们不仅能对数学成果的验证与发现产生积极作用，还会影响数学的教学与学习方式、数学知识的整理留存，以及数学思想的协作交流模式。

不过，这些演讲也兼顾了人们对人工智能的诸多担忧。我曾在论文《数学是否已过时？》https://arxiv.org/abs/2502.14874中对这些担忧进行过深入探讨，近期也以《如何看待AI人工智能时代的数学之忧》为题发表过相关演讲。我发现，将这些担忧分为两类会更便于分析，即对人工智能的一般性担忧，以及对人工智能给数学领域带来的具体影响的担忧。

对人工智能的一般性担忧，不仅涉及其对社会、经济和环境的影响，还包括其对人类独立思考与推理能力的冲击，以及将人类的生活与生计寄托于行为不可控、原理未被完全理解的系统所存在的合理性问题。我在《数学是否已过时？》一文中提出，数学至少能为解决这些问题提供部分思路，因为它让我们能够提出精准的问题，并以可独立验证、查询和审计的形式要求人工智能给出解释与论证依据。数学为我们与人工智能的互动提供了方法，让人类始终处于思考决策的核心位置，保持对自身决策的主导权。

本文探讨的是第二类担忧，即人工智能对数学行业产生的具体影响，由近期一系列值得我们深思的发展所引发。如今，技术的颠覆性已愈发明显，而我们对这一事实的重视程度远远不够。作为推动新兴技术落地的研究所所长，我或许在这场技术变革中难辞其咎，但本文的核心观点是：无论我们接受与否，人工智能已经到来，若我们无法主动迎接这一挑战，所有人都将成为这场变革的被动参与者。为了我们的学生，也为了数学学科的发展，我们必须做好这件事。

2 近期研究进展

2024年初，彼时还是帝国理工学院交换生、正在洛桑联邦理工学院访学的西德哈斯·哈里哈兰（Sidharth Hariharan）——如今是卡内基梅隆大学一年级博士生——与玛丽娜·维亚佐夫斯卡（Maryna Viazovska）展开合作，启动了维亚佐夫斯卡关于E₈格在8维球填充中最优性证明的形式化项目。如今，他们采用的方法已成为形式化学术界的标准方法：先撰写详细的非形式化蓝图，为形式化工作提供指导。（参阅zzllrr小乐数学科普文章：AI与人类协作在数学领域迎来里程碑时刻 ——21世纪菲尔兹奖获奖证明首次完成形式化验证——IEEE Spectrum）

克里斯·伯克贝克（Chris Birkbeck）与李瑞宇（Seewoo Lee）在同年夏天加入该项目，到了秋季，该项目成为西德哈斯在巴维克·梅塔（Bhavik Mehta）指导下完成硕士论文的研究基础。2025年7月，维亚佐夫斯卡（Maryna Viazovska）在英国剑桥艾萨克·牛顿研究所举办的“大证明”会议上发表演讲，汇报了该项目的进展，彼时该团队已将项目面向公众开放。

2025年秋季，项目推进十分顺利。项目负责人通过社交媒体和每周的Zoom线上会议协调志愿者团队开展研究，多家人工智能初创企业主动接洽，希望借助该项目测试其产品性能。该团队积极接纳人工智能技术，不仅接收人工智能生成的“拉取请求”，还对其进行修订以符合项目的贡献标准，并将其整合至代码库中，项目负责人也亲自参与人工智能技术的实验。

然而，几周前，西德哈斯（Sidharth Hariharan）面色苍白地来到我的办公室，他刚得知，一家名为数学公司（Math Inc.）的企业为展示其最新证明智能体高斯（Gauss）的能力，完成了该项目最终结论的形式化证明。该公司曾在11月为该项目提供过协作支持，却随后突然中止沟通，转为秘密研究。这并非该研究团队所期望的人工智能协作模式，他们从未想过，这家企业会为了取得博人眼球的成果，投入大量计算资源攻关该项目——马特·巴拉德（Matt Ballard）将这种行为贴切地描述为“过路式证明”。此后，该公司又在未获得该团队任何额外支持的情况下，利用高斯（Gauss）验证了基于8维球填充结论推导的24维球填充相关成果 https://www.math.inc/sphere-packing

Lean社区的多位知名人士，包括维护团队成员，纷纷伸出援手，协助项目负责人应对这一情况。团队的担忧之一是，该公司在新闻稿中会如何描述这一成果：高斯（Gauss）的成功，建立在人类研究者近两年的创造性工作、研究框架搭建和规划的基础之上，若将其单纯宣传为人工智能的成就，对这些主要是青年研究者的团队成员而言极不公平。

更大的担忧则是，该公司会宣称该项目“已完成”。事实上，单纯的形式化证明本身几乎毫无价值，因为维亚佐夫斯卡（Maryna Viazovska）的研究结论的正确性从未受到质疑。研究团队开展该项目，实则是为了重新梳理这些研究成果，加深对其的理解，同时构建相关库和基础设施，为未来的研究工作提供支撑。而人工智能生成的证明往往冗长繁杂，且仅聚焦于手头的具体任务，项目负责人担心，这种自私的成果抢占行为，会让团队失去修订代码、将其完善至预期状态的动力。

不过，数学公司（Math Inc.）最终与项目负责人展开合作，确保相关公告对该研究团队的贡献给予了恰当认可，并承诺将与团队公开协作，修订和优化代码以符合项目标准。如今，学界对这种人机协作模式的良好发展持谨慎乐观态度。从消极角度看，项目组织者只是在糟糕的处境中尽力挽回局面；而从积极角度看，我们都在从中学习如何让人工智能更好地服务于数学研究。目前，这一模式的发展走向仍未可知：如果人工智能能够减少形式化工作中的繁琐环节，帮助我们更好地感受和理解数学，那我们将迎来更好的发展；但如果它阻碍了我们对数学的探索乐趣和理解深度，那我们将失去一些重要的东西。

在这场形式化定理证明的风波发生的同时，数学界还见证了一场非形式化定理证明的补充实验。2月5日，11位数学家在arXiv平台发布了10道面向AI人工智能的挑战题First Proof（ https://arxiv.org/abs/2602.05192参阅First Proof首轮验证项目：数学家们组团出题考验AI（10个研究级数学问题拷问最先进AI，问题答案2月13日公布））他们的目的是评估人工智能辅助实际数学研究的能力，为此，团队挑选了各自研究中遇到的问题，这些问题均已有约5页篇幅的证明过程，但相关成果尚未发表。他们对Gemini 3.0深度思考版和ChatGPT 5.2专业版两款商用系统进行了测试，结果却不尽如人意。不过，他们也邀请了人工智能开发者用自研系统尝试解决这些问题，并要求开发者在2月13日前公开研究结果，供学界共同评估。

部分人工智能开发者响应了这一邀请，该论文的作者们委托数学计算机辅助推理研究所（ICARM）在其Zulip社交平台的相关频道开展结果研讨（http://icarm.zulipchat.com，“首轮证明First Proof”频道）并邀请数学家对人工智能的解题成果进行评价。开放人工智能公司（OpenAI）研发的模型针对其中一道问题给出的解法，被专家评价为“完全正确，且推导过程十分精妙”。表现最佳的是谷歌深度思维（Google DeepMind）研发的证明智能体阿勒西娅（Aletheia），该智能体正确解决了10道问题中的6道（https://arxiv.org/pdf/2602.21201.pdf参阅数学研究智能体Aletheia自主求解FirstProof挑战成绩6/10——由Google Gemini 3 Deep Think驱动）我想，对这样的成果表现感到惊讶的，并非只有我一人。

这些发展表明，人工智能在非形式化和形式化数学研究中的表现正愈发出色。2022年11月ChatGPT首次发布时，我们还曾嘲笑它解答数学问题的糟糕表现；而去年夏天，已有四家企业宣称其研发的人工智能系统能在国际数学奥林匹克竞赛题中取得金牌水平，其中两家的系统可生成非形式化解法，另外两家则能生成形式化解法。如今，性能顶尖的人工智能系统已逐渐攻克普特南数学竞赛的基准题。人工智能已能处理研究级的数学证明问题，这意味着，数学领域已再无“遮羞之地”。在不到四年的时间里，人工智能的定理证明能力从几乎为零发展到如今的水平，而在此期间，人工智能研发的相关投资也出现了爆发式增长。我们必须直面一个事实：人工智能很快就能比人类更擅长证明数学定理。

3 现存担忧

如今，我们陷入了一种尴尬的境地：人工智能正在完成那些我们曾认为只有人类才能做到的事。我们曾为自身的能力倍感自豪——能够解决极具难度的问题，构建逻辑严谨的长篇论证，整合众多复杂要素并做出精准的推导，但现在我们发现，人工智能也能做到这些。我们还曾为自己拥有深刻的洞见与直觉、能发现微妙的模式与关联、能构建具有深远意义的广义理论而骄傲，而当代人工智能的应用也正朝着这些方向发展。

我们需要思考，这一切会给数学行业带来怎样的影响。高校数学家的工作价值究竟何在？从某种程度来说，这份工作的存在是因为有数学专业的学生——也就是热爱数学、且父母愿意支持其学习的年轻人。我们不禁要问，若数学研究变成了向人工智能发出查询指令，这份热爱还能延续吗？

同事们常对我说，即便国际象棋引擎的水平远超人类棋手，职业棋手依然存在，但这一点安慰对我而言微不足道：我们不会要求孩子们从幼儿园到高中一直学习下国际象棋，而以国际象棋家教为业也难以维持生计。将对数学的热爱比作对音乐和艺术的热爱，或许是更贴切的类比，但音乐和艺术领域同样面临着发展支持不足的问题。如果我们为数学教学找到的最佳理由，仅仅是它能带来审美享受或休闲乐趣，那么数学的发展将举步维艰。

高校数学家的工作之所以具有实际价值，更重要的原因在于，我们为工程、商科、计算机科学、数据科学等领域开设服务性课程，而这些领域均获得了企业和政府的大力支持。但我们不难想象，这种支持也可能逐渐减少。如今，学生早已能借助人工智能完成我们数十年来布置的各类作业，而我们为了遏制这种行为设置的课堂考试，实则是人为剥夺了他们使用职业发展中必会接触到的工具的机会。如果我们不教工程师利用人工智能解决问题，那就是没有尽到培养工程师的职责，而工程学院也将不再需要我们开设的课程。我们或许不会看到相关需求一夜之间消失，但学术环境的变化日新月异，一旦根基坍塌，便难以恢复。

4 建议与展望

我们不应被上文中的悲观预警击垮，而应相信数学的力量。正如我在《数学是否已过时？》一文中所言，在人工智能时代，利用精准的语言和抽象思维帮助我们理解周遭世界、高效推理并交流思想，依然具有至关重要的意义。技术的进步为我们实现数学研究目标提供了新的途径，而人工智能终究只是一种技术，如何运用它，决定权掌握在我们手中。

在《数学是否已过时？》的结尾，我描绘了两种未来图景：一种是反乌托邦的，人类放弃数学，将思考决策的主导权让渡给人工智能；另一种则是乐观的，数学始终在思考决策过程中占据核心位置。而前文所描述的现状，大致就是反乌托邦图景的写照。那么，对数学家而言，乐观的发展图景又将如何实现？答案其实很简单：借助人工智能，更好地开展我们所熟知并热爱的数学研究。如果人工智能能助力我们实现朗兰兹纲领、证明哥德巴赫猜想、解决P≠NP问题，这难道是一件坏事吗？我们理应期待人工智能为纯数学和应用数学研究带来的裨益。如果科学家、工程师和分析师能够借助数学提供的定性和定量工具，高效运用人工智能设计出更优化的系统、取得更可靠的研究成果，那么数学的价值便已完全得以体现。

我们需要牢记自身的优势：数学家是顶尖的问题解决者和理论构建者。面对人工智能在数学领域的应用，我们不应抗拒，而应主动掌握其主动权。仅仅紧跟技术发展、为人工智能研究者设计基准测试题是远远不够的，我们需要积极参与到技术的落地应用中，让其贴合数学研究的需求。同时，我们还要学会培养学生，让他们拥有合理运用这些新技术的智慧，且务必确保核心的数学直觉与理解能力能够有效传递给学生。

找到有效运用人工智能实现数学研究目标的方法并非易事，但数学家向来乐于迎接挑战——事实上，挑战越大，我们的动力便越强。只要我们直面人工智能的到来，坚守数学研究的核心价值，数学学科必将迎来蓬勃发展。我们所需做的，只是躬身入局，潜心钻研。

参考资料

https://arxiv.org/abs/2603.03684

https://github.com/avigad

https://www.andrew.cmu.edu/user/avigad/talks.html

https://www.andrew.cmu.edu/user/avigad/Talks/lms-bcs.pdf

https://www.andrew.cmu.edu/user/avigad/Talks/rademacher1-intro.pdf

AI与人类协作在数学领域迎来里程碑时刻 ——21世纪菲尔兹奖获奖证明首次完成形式化验证——IEEE Spectrum

AI解数学题的速度比科学家编考题还快——技术飞速迭代，基准测试正以前所未有的速度过时——IEEE Spectrum

数学研究智能体Aletheia自主求解FirstProof挑战成绩6/10——由Google Gemini 3 Deep Think驱动

First Proof首轮验证项目：数学家们组团出题考验AI（10个研究级数学问题拷问最先进AI，问题答案2月13日公布）

https://arxiv.org/abs/2502.14874

https://www.math.inc/sphere-packing

https://arxiv.org/abs/2602.05192

http://icarm.zulipchat.com

https://arxiv.org/abs/2602.21201