当AI做数学时，成为数学家意味着什么？

# 人工智能在数学领域正引发重大思考 来源：https://spectrum.ieee.org/ai-in-mathematics 加州大学洛杉矶分校的陶哲轩认为，人工智能可能开启一个“大数学”时代，人类与机器协同解决复杂问题。 **大约在2000年代中期，当**杀手乐队和弗兰兹·费迪南德的音乐从我经过的每一家酒吧和夜总会传出时，我日夜挣扎在应用数学（https://spectrum.ieee.org/tag/mathematics）的博士研究中。我的研究重点是模拟特殊光波在液晶中的相互作用，并用简单方程近似理解这些互动。如今回看我的论文，液晶技术已成老黄历，我猜想如果用AI辅助，这项工作几天——甚至几小时——就能完成。 但对于我在爱丁堡大学那个拥挤办公室里的纯数学博士生同事们而言，情况却大相径庭。当时我很同情他们：日复一日坐在桌前，似乎抓耳挠腮却毫无进展。（虽然我也很挣扎，但至少总能取得一些进展。）当我们毕业各奔东西时，有些人甚至一篇文章都未发表。 现在回看，我终于理解了他们为何耗费多年钻研那些全世界只有少数人关心的抽象数学问题。并非我当初以为的傲慢——他们并非想通过率先解决看似棘手的数学问题来证明自己的超群智力。那甚至不是一种受虐倾向（这是我第二个猜测）——不是对某种想象中不足的自我惩罚。我意识到，他们从通向理解的漫长旅程中获得了快乐、满足与意义。 “有时候，理解本身让你觉得极其美好。有时候是一种成就感，就像跑完马拉松，”卡内基梅隆大学的数学家 Jeremy Avigad（https://www.cmu.edu/dietrich/philosophy/people/faculty/jeremy-avigad.html）沉思道，“但又不完全是两者中的任何一种：当你长期深入思考某个复杂困难的问题，然后——突然间——一切都迎刃而解时，那种感觉非常美妙。” 这种感觉一直驱使着历史上的数学家。同样，数学家追求这种感觉的方式几百年来也几乎没有改变。他们注意到或想象出数字、形状或逻辑结构中的联系、模式或性质，据此写出猜想——关于自己推测的未经证明的陈述。然后他们或其他数学家运用逻辑推理和数学工具，常常以有创意的方式证明或推翻这些猜想。最后，其他数学家再验证（或质疑）这些证明。 这个过程总是需要大量的思考时间。“我参加过一个纯数学夏令营，课程中我们会花半小时坐着解决困难的数学问题，没有人说话——每个人都在思考，”即将在佛蒙特大学获得博士学位的数学家兼计算机科学家 Krystal Maughan（https://kammitama5.github.io/about/）说道，“但之后我们会一起合作，慢慢梳理出问题的脉络。” 这就是数学活动中古老而永恒的乐趣。但如今的AI系统正开始切入、绕过这一缓慢而审慎的过程。把这一趋势推到逻辑极限：如果AI让数学家的苦苦挣扎变得完全多余，会发生什么？AI会不会甚至让人类彻底边缘化？ ## AI在数学中日益增长的角色 几十年来，计算一直加速着数学的进步。这始于50年前，当时数学家利用计算机证明了四色定理（https://www.ams.org/journals/bull/1976-82-05/S0002-9904-1976-14122-5/S0002-9904-1976-14122-5.pdf），该定理询问任何地图是否可以用不超过四种颜色着色，且相邻区域颜色不同。答案是肯定的，而计算机通过检查1936种情况证明了这一点（这种方式人类实际上无法验证），引起了争议。 然而，在整个计算时代，即使是在依赖巨大计算资源的证明中，人类数学家的角色仍然核心。人类凭借直觉提出猜想，凭借创造力和经验设计证明策略，然后人类验证这些证明是否正确。 如今，AI正在挑战现状（https://spectrum.ieee.org/ai-proof-verification）。短短几年内，大语言模型（LLM）从基本上只会复述从互联网抓取的基础数学内容的“随机鹦鹉”（https://dl.acm.org/doi/10.1145/3442188.3445922），演变为先进的数学推理机器。 去年夏天，来自 Google DeepMind 和 OpenAI 的系统（https://www.newscientist.com/article/2489248-deepmind-and-openai-claim-gold-in-international-mathematical-olympiad/）达到了世界数学天赋最高高中生的水平，在国际数学奥林匹克竞赛（https://www.imo-official.org/）中荣获金牌。在这项年度竞赛中，参赛者必须解决六道来自数学各领域的著名难题。 今年早些时候，Google DeepMind 的实验性AI系统 Aletheia 实现了更为重要的里程碑：它自主生成了可发表的博士级研究成果（https://doi.org/10.48550/arXiv.2601.23245）。虽然工作本身在数学上比较冷门——计算算术几何中的结构常数——但其意义在于解决一个未解决的数学问题时展示的复杂推理。而最近，OpenAI 的一个新的通用AI系统推翻了几何学中的一个重要猜想（https://openai.com/index/model-disproves-discrete-geometry-conjecture/），如果人类是作者，这一结果足以发表在主要数学期刊上。顶尖数学家称赞这一成就为AI在数学领域的里程碑，展示了独立、原创和复杂的思维。 另一个转变来自于将LLM与数学工具（即证明助手）相结合。证明助手已存在十多年，例如 Isabelle（https://isabelle.in.tum.de/）、Lean（https://lean-lang.org/）和 Rocq（https://rocq-prover.org/）——这些是专门的编程语言（https://spectrum.ieee.org/tag/programming-languages），能逐步检查数学证明，验证其逻辑正确性。传统上，数学家必须手动将定理和证明翻译成机器可读格式，即繁琐的形式化过程。现在，LLM开始消除这一瓶颈，自动将非正式证明翻译成证明助手可验证的形式化代码。 这些系统的各种版本——有时称为推理代理——正变得高度复杂。例如今年2月，AI公司 Math, Inc.（https://www.math.inc/）使用其寓意命名的推理代理 Gauss（https://en.wikipedia.org/wiki/Carl_Friedrich_Gauss）形式化了一个证明，该证明曾使瑞士洛桑联邦理工学院的数学家 Maryna Viazovska（https://people.epfl.ch/maryna.viazovska?lang=en）在2022年获得菲尔兹奖（https://www.mathunion.org/imu-awards/fields-medal/fields-medals-2022）。Gauss 首先帮助人类数学家（https://thefundamentaltheor3m.github.io/Sphere-Packing-Lean/）在几天内完成了 Viazovska 关于8维球堆积问题（https://annals.math.princeton.edu/2017/185-3/p07）解的形式化，然后自主形式化了更复杂的24维情形（https://annals.math.princeton.edu/2017/185-3/p08），仅用了两周时间。 此类成就表明，AI已经能够处理一些曾被认为是人类独有的数学任务。随着技术发展，人类数学家更多日常工作很可能成为AI涉足的领域。 ## 数学家对AI在发现中的角色展开辩论 深色西装外套、面部模糊、背景为蓝色的人像 Gluekit 人类数学家可能成为“神谕的祭司。”——杨晖·何，伦敦数学科学研究所 2025年9月，我参加了第12届海德堡获奖者论坛（https://www.heidelberg-laureate-forum.org/forum/12th-hlf-2025-1/）——这一年度会议将数百名年轻数学家、计算机科学家与他们的智力偶像聚集一堂。AI主导了讨论，从一开始，空气中就弥漫着紧张气氛。 演讲者们描述了一个未来：超越人类的AI数学家将超越人类知识与能力：形成猜想、搜索解空间、证明猜想，最后验证证明并推广结果，全程无需人类参与。如果这个未来成为现实，伦敦数学科学研究所的杨晖·何（https://lims.ac.uk/yang-hui-he/）一句名言：人类数学家可能变成“神谕的祭司”。 舞台上这些令人震惊的预言被表达出来时，我的目光被观众吸引。皱眉、坐立不安、互相交换眼神——人群的不安显而易见。澳大利亚迪肯大学的学生 Trill White（https://experts.deakin.edu.au/65467-trill-white）后来回忆坐在那个大厅里想着：“那太令人沮丧了。人类还能为数学贡献什么？会不会数学变成没人能理解的东西？我确实感觉到这将改变一切。” 长头发、面部模糊、背景为橙色的人像 Gluekit “我们当然开始意识到AI有潜力取代我们。”——Jessica Randall，Google Developer Groups 南非数学家、任职于Google Developer Groups的 Jessica Randall（https://www.linkedin.com/in/jessica-randall-293ab9205?originalSubdomain=za）表示，她感受到年轻数学家群体中对存在性恐惧的集体上升。“我能感觉到每个人都很担忧，因为他们没有想得那么远，”她说，“就像一颗重磅炸弹击中我们，我们当然开始意识到AI有潜力取代我们。” 一些资深数学家，包括何在内，似乎接受AI承担目前由人类数学家保留的任务。因为他们只想了解数学中最重大问题的答案——例如剩下的六个千年难题（https://www.claymath.org/millennium-problems/）——即使AI包办一切。“很多数学家很务实，只想理解。他们愿意为问题的答案出卖灵魂，”Avigad开玩笑说，“不惜一切代价，对吧？” 但“只想知道”阵营绝非唯一派别：大多数数学家并不希望或期望AI完全取代他们。相反，两种主流替代方案正在浮现。第一种是以人为中心、优先考虑人类对数学的理解，将AI视为工具，就像计算器一样。第二种是协作式的“团队合作成就梦想”愿景，人类和AI共同解决任何一方都无法独立解决的问题。 ## 人类在数学中的角色 菲尔兹奖得主（https://www.mathunion.org/imu-awards/fields-medal/fields-medals-2018）、普林斯顿大学数学家Akshay Venkatesh（https://www.math.ias.edu/~akshay/）多年来一直从以人为中心的视角思考这个话题。2022年，他利用菲尔兹奖研讨会（https://www.youtube.com/watch?v=N-TXcYI5C9E）恳请数学界深入研究AI可能对数学实践产生的影响。当时，AI取代数学家的想法似乎牵强。而现在，他说：“我们正在到达一个节点：至少对于某些涉及抽象数学推理的任务而言，计算机正在变得与人类有竞争力。” 对Venkatesh而言，问题不仅在于计算机能做什么，还在于数学的目的是什么。“有时候我想，当我们使用数字时，与其说我们在描述本质上数字化的现象，不如说我们能就数字的精确含义达成一致，”他说，“这是一种让我们达成共识的方式。” 一张照片显示一名女性站在满是数学公式的黑板前。 渥太华大学的Maia Fraser主张，数学不仅仅是寻找答案。对她而言，努力理解问题本身就是该学科最大的回报之一。 Markian Lozowchuk 渥太华大学的数学家兼机器学习（https://spectrum.ieee.org/tag/machine-learning）专家 Maia Fraser（https://frasermaia.github.io/）也有同感。她说她从数学中获得的快乐是人类的独特体验，融合了潜意识和意识。她描述了自己先直觉感到某件事应该正确，然后逐步提炼出能用严谨证明表达的东西。交流并分享这些深层的思考是“一种集体智慧的形态，体现了人类精神之美，”她说。 根据这些论点，AI对一个顽强抵抗人类努力的数学猜想的证明，只有对人类可理解时才有用。“语句能被AI证明本身就是有用的信息，”Fraser承认，“但设计出优雅优美的人类证明仍然是开放问题。”即使不存在这样的证明，她表示，寻找它“依然是有价值的努力。” ## AI与数学合作的未来 一种更协作的AI融入数学的方式来自陶哲轩（https://www.math.ucla.edu/~tao/），他10岁首次参加数学奥林匹克。1986、1987、1988年分别获得铜牌、银牌和金牌，成为奥林匹克历史上最年轻（https://en.wikipedia.org/wiki/List_of_International_Mathematical_Olympiad_participants）的三种奖牌得主。如今他是菲尔兹奖得主（https://www.mathunion.org/imu-awards/fields-medal/fields-medals-2006）和加州大学洛杉矶分校教授，被誉为在世最杰出的数学家之一。 与他的一些同龄人不同，陶哲轩对AI既不轻视也不恐惧。相反，他视其为学科根本转变的催化剂——向着他所称的“大数学”过渡。他构想了人类与机器之间大规模、去中心化的协作未来，数学任务可以被切分和细分，人类承担创造性部分，而AI承担大部分技术性繁重工作。 陶哲轩已经在实验这一概念，与众多在线合作者一起研究问题（https://github.com/teorth），其中一些使用AI工具。“一百年前，几乎每篇数学论文都是单一作者，”他说，“但现在我和素未谋面的人合作——也许未来我甚至不知道他们是AI还是真人。” 陶哲轩愿景的关键在于独特的数学概念：形式化。当一个证明被翻译成代码，并由证明助手逐步检查时，就消除了任何人错误（https://spectrum.ieee.org/tag/human-error）或不诚实的机会。这种方法改变了合作方式，因为信任通过验证而非声誉或关系建立。来自陌生研究员甚至业余爱好者的想法，如果附有形式化证明，就能被认真对待。 “如果没有