数学家心声：《论AI与数学的进步：梦想一台数学通用机器》by 文森特·朗格（Vincent Runge）2026-10-27
★置顶zzllrr小乐公众号，追踪《小乐数学科普》系列报道，参与数学 vs AI投票！
坚持不炒作的数学与AI报道，投稿信箱zzllrr@gmail.com
论人工智能与数学的进步：
梦想一台数学通用机器
作者：文森特·朗格（Vincent Runge）
巴黎-萨克雷大学埃夫里分校副教授，埃夫里数学与建模实验室。
他的研究重点是变点检测和结构化数据的高效算法，从事动态规划和剪枝方法、非欧几里得空间的扩展，以及用于时间序列分析的计算几何。
日期：2026-10-27
摘要
2026年秋，数学正面临其历史上或许最为深刻的危机。数学知识借以生产、验证、传播与评估的整个生态系统，正开始瓦解。数学系——那些通常安静而文明的地方——突然陷入动荡，成为一场新的"古今之争"意想不到的剧场。危机之源是清楚的：AI 系统在证明与验证数学结果方面，已经超过了哪怕最优秀的人类数学家。
本文为数学活动提出一个比喻：我们曾把自己想象成登山者；不久之后，我们可能变成在数学矿井中挖掘的矿工，与数学 AI 机器或协作、或竞争。届时，发表将主要被视为帮助人类理解数学的手段，而对数学进步的度量则交给一台数学通用机器。本文以非技术的方式探讨这个"美丽新世界"式的数学可能是什么样，以及我们如何共同塑造它的未来。
"自由不可分割：你不能切除其中一部分而不把整体杀死。"
—— 米哈伊尔·巴枯宁（Mikhaïl Bakounine），1895
1 人类的冒险
自由与创造力是数学家最珍视的价值之一。年复一年，我们耐心地建造内心世界，在其中，抽象概念逐渐变得熟悉，而且奇怪地几乎变得具体。一步一步，我们成为自己那颗小小星球的探索者，熟悉每一条路径、每一个地标、每一个隐秘的角落。我们为成为某个特定主题上的参照——哪怕只是一个微小的参照——而自豪。在这片小小的疆域里，我们获得了判断新想法的能力。
图：圣埃克苏佩里《小王子》（1943）中的地理学家。
我们分享对真正新颖之物的热情，并耐心解释那些并不新颖的东西。我们鼓励新一代学生冒险进入数学的美丽风景。然而有了 AI，我们有可能变成圣埃克苏佩里那本名著中的地理学家：他从不离开书桌，甚至说不出自己的星球上有没有海洋或山脉——他等着探险者来告诉他。明天，探险者可能是机器，这将限制我们的自由、枯竭我们的创造力。
我们也热爱与同行分享这份知识，而我们分享的许多内容，是出奇私密的想法：难以形式化的直觉、疑虑、半成形的类比、以及失败的记忆。其中一些同行成为挚友。我们喝掉很多咖啡¹，在黑板前站上好几个小时。我们画图、发明比喻，试图让彼此看见自己开始看见的东西。有时我们会遇见巨人：那些名字我们熟知多年、来自当年看来难得不可能的论文的数学家。我们感谢他们，我们敬仰他们。
然后，有时，其中一位读到了我们写的东西，在短暂的一瞬，我们看见他们眼中一丝认可的光。我们继承故事，也继承定理。深夜里，在会议晚宴上，一位年长的数学家给我们讲一段关于埃尔德什、格罗滕迪克或阿诺德的轶事。这些故事不在书里，却把我们与数学的深远过去连接起来。它们提醒我们：数学是一座巨大的建筑，它的建造者即便离去，也以某种方式仍在我们中间。
¹ 我们知道那句名言："数学家是把咖啡转化为定理的装置"，它常被归于 Alfréd Rényi（阿尔弗雷德·雷尼），但常被误归为 Paul Erdős（保罗·埃尔德什）。
在这个意义上，每一位数学家都是一座古老而奇特的博物馆的馆长，手中握着一把钥匙。当他们给予我们这份殊荣时，便带我们进行一场私人导览。他们不仅向我们展示展厅里陈列着什么，还告诉我们它为何重要、它如何来到这里、哪些门通向虚无、哪条被遗忘的通道或许仍值得打开。书籍、论文和维基百科里含有数学，但它们是冷冰冰地含有它。
数学的鲜活体验是另一回事：它在于向他人学习并分享所学，在于直觉、品味、故事、热情与观看方式的传递。这一切，以及更多，构成了数学的人类冒险。当一台机器替我们写下定理，我们还会在意、还会联结、还会投入这场冒险吗？
图：喷气推进实验室（JPL）里一支被称为"计算机"的才华横溢的女性团队。
数学活动极为艰难。一代又一代，我们耐心地建造数学的珊瑚礁：概念叠着概念，定义叠着定义，证明叠着证明。我们填补学科之间的空隙，在相距遥远的思想之间架桥，并慢慢把孤立的结果转化为连贯的知识体。AI 改变了这场游戏。我们受训去证明，而突然间，证明本身作为一种人类独有的技能，面临被淘汰的风险。
这就好像我们花了多年学习手算大数的乘法，结果有人把计算器放到了桌上。这个类比并不像初看时那样只是比喻。几个世纪以来，计算本身就是一项人类活动。二十世纪上半叶，女性被雇为"人肉计算机"，用手工进行计算，直到电子计算机逐渐接管这项工作。其中一些女性后来成为最早的一批程序员。
类似的事情如今可能正发生在数学家以证明为业的活动上：机器最初对计算所做的，现在可能开始对证明做。我们正从一个由人类理解主导的时代，走向一个必须与机器理解周旋的时代。数学各领域之间的新证明、新联系与新插值，如今可以以某种速率被生产出来，而这个速率可能很快超过数学共同体以往的任何经验。我们数学文化赖以建立的稀缺，正开始消失。当证明变得过剩，新的稀缺又在哪里？
图：H.G. 威尔斯《世界脑》（1938）与《新世界秩序》（1940）。
这些引言对数学家来说都不是新闻。它只是阐明了为什么当下的转变让人感到如此受威胁。我们害怕与数百年的智识生活传统决裂，进入一个晦暗而不确定的世界，在其中人类的数学理解被逐渐抛在后面。我们想守住最珍视的东西：智识的独立、自由、普遍性、开放性，以及亲自理解数学的乐趣。
但还有另一种危险。数学建立在格外牢固的信任、正直与思想诚实规范之上。AI 有可能从瓶子里放出最糟糕的精灵之一：猜疑。"不用 AI 的数学家"与"借助 AI 的数学家"之间的分野，可能会撕裂共同体。因此，我们需要一个环境，使人类的数学活动既能被保存、又能被转化。由论文、同行评议、期刊、引用与声望构成的旧体系并不完美；面对机器生成的大量数学，它可能越来越力不从心。我们的提议是将人类理解的推进与数学进步的度量部分地脱钩：保护前者，同时发展新的工具来度量与组织后者。
这需要为新世界秩序建立一个新的机构：数学通用机器（Mathematical Universal Machine，MUM），一套供整个数学共同体使用的共享 AI 基础设施。它将延伸 H.G. 威尔斯"世界脑"[35] 的愿景（关于这一段历史，见附录 A，由 AI 生成！）。这台机器还将提供数学进步的定量度量，作为传统同行评议体系的补充。设计这台机器并度量它的行为，本身就是一项巨大的数学任务。下面我们呈现这样一个系统可能的样子。
2 数学通用机器
2.1 矿井与矿工：地图、工具、大脑与预算
在这个 AI 辅助数学的新世界里，我们提出"数学矿井"的比喻。矿井是数学真理的空间。数学成果是藏于其中的钻石；证明是通向它们的巷道。数学 AI 系统就是矿工。它的目的是通过以某种程度的独立自主做出自己的决策来在这片空间中导航，从而完成任务。这里的表述仅限于非常一般的术语。一次借助 AI 的检索，把我们引向了精确得多的想法，任何人都可以轻松复现。
我们考虑由三个不同部分组成的矿工：
矿工持有通向已知钻石的地图。它们对应研究论文、已证成果数据库、定义、概念、定理之间的结构化依赖图等。他可以在任何时刻使用它们来提升自己的搜索能力。
矿工还可以使用外部工具，例如用于形式验证的 Lean、用于实验的 Python 与计算机代数。这些工具让他在矿井中的工作更轻松，帮助他探索、验证、测试和定向。
矿工有一个大脑：AI 系统的核心，一个拥有数十亿学习参数的大语言模型。它使他能够自主工作：搜索证明、检验猜想、使用外部工具，并以自己的探索策略决定下一步探索什么。这个大脑体现了他内化的数学直觉、表征、启发式，以及决定在哪里挖、如何挖的能力。重要的是，矿工还有记忆，记得自己已经采取过的行动，从而能从失败的尝试中学习，避免反复走上同一条路径。
在矿工结构之外，这台机器具有有限的耐心，用有限的计算预算来表示。他的精力受人类设计的系统限制，而这个系统的计算资源最终必须在所有数学家之间共享。这种限制也可能是刻意设定的：我们或许会选择阻止过长的探索，因为那样可能把矿工带入未知疆域太远。我们也可能选择建造一个最小能耗的系统，其"数学能力与能耗之比"成为数学研究的新目标。
在这些部分都固定之后，AI 系统可以完成交给它的一些工作。与此同时，任由这样一个系统自由探索数学，会导致我们所说的矿井的凸化（convexification）：机器逐步填满从已知出发可达的数学疆域。新结果被发现，新定理被证明，新定义浮现，更简单的证明被找到，此前彼此分离的区域之间的联系被揭示。所有这些新数学，都因这台机器而成为可能。
然而我们假设，人类的智识与想象力不会被机器完全吞并。有些数学工作可能仍位于这种凸化之外：呈现已知数学的新方式、出人意料的定义或视角，或者机器无法自行发现的真正原创的研究。这些贡献一旦被整合进机器，就会扩大它的可达疆域，并启动新一轮凸化过程。这一视角提示了两种不同而又互补的数学研究方式：
数学家作为监工。
数学家通过 AI 系统探索数学，在矿井中监理矿工。使用者指挥 AI 大脑，并把它的工作约束在自己作为数学家的专长范围内，告诉它探索什么，提出搜索方向与想法。机器在人的帮助与反馈下寻找新结果，同时不断学习如何在工具、地图、记忆、计算等之间更好地使用自己的能力。在实践中，这可能发展成一门向 AI 系统"下提示"的艺术，涉及复杂的指令序列、反馈、重新定向，以及随着探索展开而进行的介入。
数学家作为矿工。
数学家在机器之外工作，亲自探索矿井，寻求超出机器当前触及范围的数学。由此产生的论文提供新的地图，通过"机器更新"可能被内化进矿工的大脑，改变它此后探索数学的方式。在这种模式中，数学家刻意限制对机器的依赖：跟得太紧，就有停留在机器已探索过的疆域、而非冒险越过其当前凸化的风险。
这两种模式代表了数学研究的互补路径：要么监理并引导矿井的探索者，要么自己仍是矿工，以更传统的探索形式从事数学。为支持这两种研究，我们需要引入新的度量，用于评估数学产出、量化数学家在各个角色中的贡献。
2.2 机器视界
图注：机器视界（水平 p）——机器在预算之内、在其全部能力（凸包）之内以高概率到达的区域；灰度表示成功概率 pᴍ(T|B)，由高到低；中心浅蓝区域为机器的先验知识；外部红色轮廓为机器的全部能力（凸包）。
我们形式化地表示数学通用机器（即矿工）：M=(θ, 𝒦, 𝒯)，其中 θ表示它的大脑，𝒦表示它的数学地图，𝒯表示它的外部工具。
矿工在有限的计算预算 B下运行，B以数学研究计算单位（Mathematical Research Compute Units，MRCU）度量：这是一个需要精确定义的量。
对于目标命题T，我们定义成功概率为
pᴍ(T|B) = Pr(M 在预算B 内证明T)
其中 T 是人类已知的、但被排除在机器先验知识之外的命题。对给定的概率p∈(0,1)，机器视界是矿工在其计算预算内能够到达的数学结果集合：
ℋᴍ(B; p) = { T : pᴍ(T|B) ≥ p }
这个视界代表机器可触及的数学疆域：在它之外，是矿工以其当前的大脑、地图、工具与计算资源无法可靠发现的真理。（关于这一想法的历史，见附录 B。）
图：《来自天书的证明》（Proofs from THE BOOK）第一版（1998）。
扩展机器视界 ℋᴍ(B; p)呼应了保罗·埃尔德什关于那本"天书"（The Book）的愿景：一本想象中的书，上帝在其中保存着每个数学定理最美的证明²。这一愿景启发了 Martin Aigner 与 Günter M. Ziegler 的《来自天书的证明》，一本礼赞格外优雅的数学证明的合集。
我们的提议追求一个相关的目标：与其为每个定理寻找最美的证明，我们寻求通过提升矿工发现它们的能力，使数学真理变得越来越可及。正如一则来自"那本书"的证明揭示了通往某个数学真理的出人意料之优雅路径，一台能力更强的机器也可能揭开通往数学矿井整片区域的更短路径。
² 正如埃尔德什的名言："你不必相信上帝，但你应该相信那本天书。"
改进机器需要新的度量来评估它的进步。今天，数学家的工作通过漫长的人工同行评议过程来评估。如前所述，发表可以服务于推进人类理解，而不是度量数学进步。数学通用机器将提供数学进步的定量度量，并帮助把个人与集体的贡献归因于数学发现。
机器将按固定周期纳入新发表的成果进行更新，这不仅带来新的数学地图，也带来矿工大脑参数的更新：θₜ→ θₜ₊₁。
每次机器更新之后，将重新评估它的数学能力，特别是通过度量证明某个定理的概率变化 pᴍₜ(T|B) 、以及其视界的扩张 ℋᴍₜ(B; p) 来衡量。
我们也可以度量发现数学结果所需计算量的减少，从而估计一项贡献在多大程度上提升了机器探索矿井的能力。这样的度量可以为认可数学家的贡献提供新的依据——无论他们是自己发现了新数学，还是通过人类监理改进了机器的探索。
这一关于数学新组织的愿景——工业化的数学工作与手工的数学工作并存——仍然是推测性的，开发一个能调和两者的系统的可能性同样如此。它的实现将取决于我们能否开发出能力与局限都被更好理解的数学 AI 系统。
3 政治性的项目
数学家在社会、科学与技术的看法上往往是进步主义的。作为科学家与公民，我们中的许多人也深切关心生态与气候变化。AI 当前的发展轨迹并不是我们所梦想的。AI 消耗大量的能源、水、土地和物质资源。当它与监控、社会控制或战争联系在一起时，其使用也引发严重的伦理关切。
面向数学的 AI 目前集中在少数私营公司手中（大多位于美国），它们最强大的模型只对经过挑选的合作者开放。与此同时，把这些系统用于数学所带来的负面物理影响，仍然缺乏良好的度量与记录。大多数数学家发现很难接受现状。
我们不应安于现状。我们可以组织起来、集体行动，提出一个更好的模式。我们可以建设一套面向数学的通用 AI 基础设施：与联合国教科文组织（UNESCO）这样的国际机构合作开发，由数学家通过一个专门的国际组织（例如IMU国际数学联盟）治理。
在各国政府、大学与慈善机构的支持下，它将属于全球科学公域，而不是留作少数私人行为体控制的专有资产。这台数学通用机器（MUM）将围绕数学共同体的价值来建造。作为起点，它可以依据以下原则治理：
生态责任。其能源消耗、环境影响与物质足迹每年由独立机构评估并公布。
开放架构。模型的架构、权重以及系统的关键组件将公开可及。
普遍而平等的接入。向数学共同体开放（可能包括学生），每位用户享有同等的计算或 token 预算。
隐私。用户对自己的数据保有完全控制。私人研究、未发表成果以及提交给系统的预印本，未经明确同意绝不并入共享系统。
透明的机器更新。每年一次，用新发表的数学与符合条件的预印本更新数学数据库与矿工的大脑。随后将估计每项新的与既有贡献的计算重要性。
国际科学治理。一个数学—计算机科学的联合实验室（设于 UNESCO 之内或与之合作）将负责机器更新、维护、评估与沟通。
数学家常常用登山的比喻来描述自己的研究。经过巨大而孤独的努力，我们抵达峰顶，从那里眺望一片广袤的、尚未探索的数学真理之景。正如陶哲轩所指出的，我们如今可能正在见证数学浪漫时代的终结——孤独英雄的时代（陶哲轩：从数学1.0迈向数学2.0——科学×AI峰会报告全文2026-10-16）。从山上，我们下到矿井：一片充满机器、出人意料的发现与颠覆性创新的工业化景观。
据一则著名的轶事，当有人问约翰·冯·诺依曼，一个人有望理解数学的百分之多少时，他回答："大约 28%。"有了这台机器，我们或许能重拾十九世纪理想的一丝余韵——那时，顶尖数学家仍可期望对数学整体获得综合性的理解。
在矿井的泥泞中，我们有能力集体地组织这场探索、守住我们的理想，或许还亲手建造工业数学的时代。在这场转变之中，有一条真理不变：我们已被从山上送入矿井。对于进步，无药可解³。适应不是可选项；守住我们的价值与部分工作习惯，仍然是可能的。
³ John von Neumann, "Can We Survive Technology?", Fortune, June 1955.
（AI 建议在文档中加入以下附录，并生成了它们，仅做了少量人工修正。）
附录A 共享的知识
每一代数学家都重新发明了自己分享所知的方式，也随之重新发明了给予认可的方式。这部历史读起来就是科学期刊缓慢解绑的过程（表 1）。MUM 将是它的下一步，也是机器本身首次成为贡献者的一步。
在期刊之前，信件承载着数学：马兰·梅森（Marin Mersenne）的通信为他赢得了"欧洲的邮箱"之名。1665 年，《学者杂志》（Journal des sçavans，巴黎，1 月 5 日）与《哲学汇刊》（Philosophical Transactions，伦敦，3 月 6 日）把至今仍依赖的四项功能捆绑在一起：登记谁最先发现什么、认证结果、使之被知晓、以及存档 [26]。
狄德罗与达朗贝尔的《百科全书》（1751–1772）[7] 增加了一张地图——达朗贝尔的知识树，并用交叉引用把条目链接起来；当它的出版特权在 1759 年被撤销时，最后几卷是秘密完成的。
自 1868 年起，《数学进展年鉴》（Jahrbuch über die Fortschritte der Mathematik），以及后来的 Neugebauer 的《数学文摘》（Zentralblatt，1931）与《数学评论》（Mathematical Reviews，1940），为整个文献绘制了地图，如今以 zbMATH Open 的形式免费开放；诸如 OEIS（1964）[22] 这样的对象数据库随后出现。它们是第 2 节中地图 K 的先祖。
1930 年代，布尔巴基以结构的共同架构、在一个集体笔名下重写了数学 [3]，并成为一种单一文化：谁设计了共享的架构，谁就塑造了什么算作数学。H.G. 威尔斯的《世界脑》[35] 呼吁持续修订与在世界各地散布副本，这两个想法以年度机器更新与第 3 节的开放架构的形式回归，而避免了后来的读者所批评的中央集权倾向 [25]。
arXiv（1991）[10] 把传播与认证分开：预印本即时流传，时间戳确定优先权，把认证单独留给期刊。第 1 节提出的脱钩又进一步把认证拆开：证明助手检查正确性，MUM 将度量进步，而发表将服务于人类理解。
Polymath（2009）[13] 把第 1 节所述研究的私密一面公开化，并找到了密度 Hales–Jewett 定理的一个新证明，署名 D.H.J. Polymath [24]；但没有任何招聘委员会能评估一个化名的份额。
等式理论项目（Equational Theories Project，2024）结合人类证明、自动证明器与 Lean，解决了 4694 条原群（magma）定律之间全部 22028942 条蕴涵，并记录了谁贡献了什么 [2]：一个 MUM 的小规模原型。陶哲轩原群等式定律——数学家群体合作大项目440天基本收官，就差临门一脚！
与此同时，认可开始被计数：引文索引 [9] 与 h 指数 [16]；在报告《引文统计》（Citation Statistics）中，国际数学联盟曾警告不要用这类数字进行排名 [1]。MUM 不会去数引用，而是估计一项工作对机器可达范围所造成的差异（第 2 节），作为对人类判断的补充。
当获取知识的通道受到威胁时，数学家也曾集体行动：《拓扑学》（Topology）的编辑在 2006 年集体辞职 [17]，2012 年数千人加入"知识的代价"（The Cost of Knowledge）抵制运动 [29]。建造一台公共的机器（第 3 节）是同一场斗争，只是换了新工具。
表 1：数学知识的分享，从最初的期刊到 MUM
| | | | |
|---|---|---|---|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
附录 B 将数学推理机械化
MUM 背后的第二个传统追问：推理是否像此前的计算那样（第 1 节），可以被机械化。它的回答就是第 2 节的模型：不是一种判定每个命题的程序，而是一场带有预算与成功概率的搜索。按顺序读下来，它给出了矿工 M=(θ, 𝒦, 𝒯)的各个组成部分以及他的预算 B（表 2）。
表 2：数学推理的机械化，从莱布尼茨到 MUM
| | | | |
|---|---|---|---|
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
| | | | |
莱布尼茨希望争端能通过计算来解决，双方互道"让我们计算"（calculemus）[18, 200]：这是对第 1 节所述猜疑的一种早期回答，因为经过检验的证明无需信任。
弗雷格，然后是怀特海与罗素，建立了形式语言 [8, 36] 并揭示了它的代价：1+1=2 只能由《数学原理》的命题 *54.43 推出。
希尔伯特要求一种判定每个命题的程序 [15]。
哥德尔表明，任何一致、有效公理化且包含算术的理论，都会留下某些不可证明的真理 [11]：从给定的地图出发，某些钻石在任何预算下都无法触及。
图灵表明没有算法判定可证性 [32]。证明仍可被逐一列出，因此无限制的搜索最终会找到每个可证命题，但没有人能事先知道某个给定命题会在何时出现、或是否会出现：这就是第 2 节凸化的极限，也是搜索必须被截断的原因。
在同一篇论文中，图灵描述了通用机器；MUM 在图灵的意义上是通用的，在《世界人权宣言》第 27 条的意义上也是通用的——人人有权"分享科学进步及其带来的利益"[34]，这为第 3 节的平等接入提供了依据。
不可判定性留下了实践中真正重要的问题：寻找证明的代价。1956 年，哥德尔写信给当时病重中的冯·诺依曼：机器很容易判定一个命题是否有长度为 n 的证明，但它的运行时间必须随 n 增长得多快？如果只是线性或二次增长，"数学家关于是/否问题的脑力工作就可以被机器完全取代"[28]。
这个问题后来以 P 与 NP 问题重现，最初正是针对定理证明程序提出的 [4]，至今仍未解决：检验一个证明很容易，找到它似乎很难。这种不对称组织了 MUM：验证便宜而确定，是工具 T 的工作；搜索昂贵而不确定，是大脑 θ在预算 B下的工作。视界 ℋᴍ(B; p) 以经验的方式提出哥德尔的问题：不是最坏命题的代价如何增长，而是一个给定的矿工用自己的预算能走多远。
于是机器开始搜索，也开始检验。Newell、Shaw 与 Simon 的 Logic Theorist（1956）[21] 证明了《数学原理》前 52 个定理中的 38 个，其中一个比怀特海与罗素的更优雅，这是"那本书"（第 2 节）的早期回响；据说有一篇把该程序列为合著者的论文被拒。
1996 年，证明器 EQP 解决了悬置六十年的 Robbins 问题 [20]：机器抵达了一颗人类未曾到达的钻石。与此同时，计算进入了证明，猜疑也随之而来：没有审稿人能手工重做四色定理（1976）背后的计算机检验，开普勒猜想的审稿人也只是"99% 确定"。
证明检查器——从 Automath、Mizar 到 Coq 与 Lean [5, 6]——用两个定理的形式化证明（2005 与 2014）[12, 14] 消除了疑虑，把信任从审稿人转移到验证。
QED 宣言（1994）呼吁建立一个统一的、经过验证的数学库 [31]，但陷入停滞 [37]；此后 mathlib 在开放环境中建成了这样一个库 [30]，而"液态张量实验"（2022）把它带到了当前的研究前沿 [27]。
大脑是最后到来的。Logic Theorist 的启发式是手工编写的；今天证明器的启发式则是从地图中学来的。2020 年，一个在形式数学上训练的语言模型引导了证明搜索，并向 Metamath 库贡献了证明 [23]；2025 年，AI 系统在国际数学奥林匹克上达到金牌水平 [19]。
由于大脑是从地图中学来的，新的地图会改变大脑：这就是第 2 节的机器更新 θₜ→ θₜ₊₁ 。这类证明器如今已经用在固定的尝试次数内证明基准命题的比例来评分 [38]：这就是 pᴍ(T|B)，只是没有这个名字。MUM 将增加规模与开放性：把整个数学作为基准，并建立一个让地图、工具、大脑与预算保持开放与共享的机构（第 3 节）。
图灵曾点出那个未决的问题。1939 年，他把数学推理描述为"两种能力的结合运用，我们可以称之为直觉与机巧（intuition and ingenuity）"，并回顾说"在哥德尔之前的时代"，有人曾希望用形式规则取代一切直觉判断 [33]。
哥德尔的信追问的是：机巧能否被高效地机械化；学习型证明器则提示，直觉的一部分是可以学到的。是否全部都能学到，就是第 2 节的假设，而 MUM 正是为检验它而设计的。
原文参考文献
[1] R. Adler, J. Ewing, and P. Taylor (2009) Citation statistics. 24 (1), pp. 1–14. Cited by: Appendix A.
[2] M. Bolan, J. Breitner, J. Brox, N. Carlini, M. Carneiro, et al. (2025)The equational theories project: advancing collaborative mathematical research at scale(Website) External Links: 2512.07087 Cited by: Appendix A.
[3] N. Bourbaki (1939) Éléments de mathématique. Hermann. Cited by: Appendix A.
[4] S. A. Cook (1971) The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC), pp. 151–158. Cited by: Appendix B.
[5] N. G. de Bruijn (1970) The mathematical language AUTOMATH, its usage, and some of its extensions. In Symposium on Automatic Demonstration, Lecture Notes in Mathematics, Vol. 125, pp. 29–61. Cited by: Appendix B.
[6] L. de Moura, S. Kong, J. Avigad, F. van Doorn, and J. von Raumer (2015) The Lean theorem prover (system description). In Automated Deduction – CADE-25, Lecture Notes in Computer Science, Vol. 9195, pp. 378–388. Cited by: Appendix B.
[7] D. Diderot and J. L. R. d’Alembert (Eds.) (1751) Encyclopédie, ou dictionnaire raisonné des sciences, des arts et des métiers. Cited by: Appendix A.
[8] G. Frege (1879) Begriffsschrift. Louis Nebert. Cited by: Appendix B.
[9] E. Garfield (1955) Citation indexes for science: a new dimension in documentation through association of ideas. 122 (3159), pp. 108–111. Cited by: Appendix A.
[10] P. Ginsparg (2011) ArXiv at 20. 476, pp. 145–147. Cited by: Appendix A.
[11] K. Gödel (1931) Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. 38, pp. 173–198. Cited by: Appendix B.
[12] G. Gonthier (2008) Formal proof—the four-color theorem. 55 (11), pp. 1382–1393. Cited by: Appendix B.
[13] T. Gowers and M. Nielsen (2009) Massively collaborative mathematics. 461, pp. 879–881. Cited by: Appendix A.
[14] T. Hales et al. (2017) A formal proof of the Kepler conjecture. 5, pp. e2. Cited by: Appendix B.
[15] D. Hilbert and W. Ackermann (1928) Grundzüge der theoretischen Logik. Springer. Cited by: Appendix B.
[16] J. E. Hirsch (2005) An index to quantify an individual’s scientific research output. 102 (46), pp. 16569–16572. Cited by: Appendix A.
[17] A. Jackson (2007) Jumping ship: Topology board resigns. 54 (5), pp. 637–639. Cited by: Appendix A.
[18] G. W. LeibnizC. I. Gerhardt (Ed.) (1890) Die philosophischen Schriften. Vol. 7, Weidmann. Cited by: Appendix B.
[19] T. Luong and E. Lockhart (2025)Advanced version of Gemini with Deep Think officially achieves gold-medal standard at the International Mathematical Olympiad(Website) Google DeepMind. External Links: Link Cited by: Appendix B.
[20] W. McCune (1997) Solution of the Robbins problem. 19 (3), pp. 263–276. Cited by: Appendix B.
[21] A. Newell and H. A. Simon (1956) The logic theory machine: a complex information processing system. 2 (3), pp. 61–79. Cited by: Appendix B.
[22] OEIS Foundation Inc.The on-line encyclopedia of integer sequences(Website) External Links: Link Cited by: Appendix A.
[23] S. Polu and I. Sutskever (2020)Generative language modeling for automated theorem proving(Website) External Links: 2009.03393 Cited by: Appendix B.
[24] D. H. J. Polymath (2012) A new proof of the density Hales–Jewett theorem. 175 (3), pp. 1283–1327. Cited by: Appendix A.
[25] W. B. Rayward (1999) H. G. Wells’s idea of a World Brain: a critical reassessment. 50 (7), pp. 557–573. Cited by: Appendix A.
[26] H. E. Roosendaal and P. A. T. M. Geurts (1997) Forces and functions in scientific communication: an analysis of their interplay. In Co-operative Research in Information Systems in Physics (CRISP 97), Cited by: Appendix A.
[27] P. Scholze (2022) Liquid tensor experiment. 31 (2), pp. 349–354. Cited by: Appendix B.
[28] M. Sipser (1992) The history and status of the P versus NP question. In Proceedings of the 24th Annual ACM Symposium on Theory of Computing (STOC), pp. 603–618. Cited by: Appendix B.
[29] (2012)The cost of knowledge(Website) External Links: Link Cited by: Appendix A.
[30] The mathlib Community (2020) The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), pp. 367–381. Cited by: Appendix B.
[31] (1994) The QED manifesto. In Automated Deduction – CADE-12, A. Bundy (Ed.), Lecture Notes in Computer Science, Vol. 814, pp. 238–251. Cited by: Appendix B.
[32] A. M. Turing (1936) On computable numbers, with an application to the Entscheidungsproblem. 42, pp. 230–265. Cited by: Appendix B.
[33] A. M. Turing (1939) Systems of logic based on ordinals. 45, pp. 161–228. Cited by: Appendix B.
[34] United Nations General Assembly (1948) Universal declaration of human rights. Note: Resolution 217 A (III) Cited by: Appendix B.
[35] H. G. Wells (1938) World brain. Methuen. Cited by: Appendix A, §1.
[36] A. N. Whitehead and B. Russell (1910) Principia mathematica. Vol. 1, Cambridge University Press. Cited by: Appendix B.
[37] F. Wiedijk (2007) The QED manifesto revisited. 10 (23), pp. 121–133. Cited by: Appendix B.
[38] K. Zheng, J. M. Han, and S. Polu (2022) miniF2F: a cross-system benchmark for formal olympiad-level mathematics. In International Conference on Learning Representations (ICLR), Cited by: Appendix B.
求点赞
求分享
求喜欢
参考资料
https://arxiv.org/abs/2610.35263
https://proofsandprompts.com/2026/11/12/on-ai-and-progress-in-mathematics-dreaming-a-mathematical-universal-machine/
【未来数学畅想系列】很多年轻数学家猜测2026是最后一届人类菲尔兹奖年？你怎么看
数学的未来（上篇）：理解数学与创造数学 by 费德里科?阿斯基耶里（Federico Aschieri）2026-10-9
数学的未来（第二篇）：数学家的使命——AI时代下数学家的角色 by 费德里科?阿斯基耶里（Federico Aschieri）2026-10-24
小乐数学科普：从三体宇宙到数学宇宙——致敬《三体》发表20周年
MIT麻省理工学院数学系《未来的数学》by Pavel Etingof、Slava Gerovitch 2026-10-6
数学家心声：《数学的未来图景》by 弗洛里安·布鲁尔（Florian Breuer）2026-10-26
小乐数学科普历年合集
《小乐数学科普》2026年10月精选文章目录
《小乐数学科普》2026年Q3精选文章目录
zzllrr小乐微信公众号栏目《小乐数学科普》2026年6月文章精选
zzllrr小乐微信公众号《小乐数学科普》2026年5月文章精选
《小乐数学科普》2026年4月文章精选
2026Q1《小乐数学科普》精选文章合集目录
近三月《小乐数学科普》精选文章合集目录202512—202602
2026年01月《小乐数学科普》精选文章合集目录索引
2025年《小乐数学科普》精选文章合集目录索引
《小乐数学科普》2024年合集
· 开放 · 友好 · 多元 · 普适 · 守拙·
让数学
更加
易学易练
易教易研
易赏易玩
易见易得
易传易及
欢迎评论、点赞、在看、在听
收藏、分享、转载、投稿
点击左下角 阅读原文
查看原始文章出处
点击底部一起捐
助力腾讯公益
点击zzllrr小乐
公众号主页
右上角
置顶★加星
数学科普不迷路！
原标题：《数学家心声：《论AI与数学的进步：梦想一台数学通用机器》by 文森特·朗格（Vincent Runge）2026-10-27》