具身理解：数学的危与机

写在前面

今天，OpenAI 发布了一份声称解决有理数域上希尔伯特第十问题（H10/ℚ）的数学手稿。消息传来的那一刻，我正在做另一件事。

我是一家建材家居企业试用期的外贸业务员。今天公司新办公室刚装修完，我和同事们用抹布擦去窗框上的粉尘，铲掉地板上残留的胶痕，把新到的样品板一块块摆上展示架。空气里弥漫着油漆、胶水和木屑的气味，指缝里塞满细灰。正是在搬完最后一箱瓷砖样品、坐在窗边短暂休息的时候，我看到了那条消息。屏幕上，H10 的证明、Lean 代码、arXiv 链接、数学界的即时评论像潮水一样涌来；脚下，是刚擦过的地面。

我翻开手边的笔记本，一段话静静躺在那里：

“我自己在北京的生活条件很差，可是在另一方面，古都的景色是鲜艳而生动的，这对我是一个补偿。但是在公园里和故宫广场上，我却看到了北方的早春。当北海仍然结着冰的时候，我看到白梅花盛开。我看到北海的垂柳，枝头悬挂着晶莹的冰柱，因而想起唐朝诗人岑参咏雪后披上冬装的树木的诗句：‘千树万树梨花开。’北京数不尽的树木引起了我的惊叹和赞美。”

这段话出自毛泽东向埃德加·斯诺讲述早年北京生活的自述，记录于《西行漫记》（出处见“注释与出处”）。一边是冰封的北海与盛开的梅花，一边是以毫秒计算的算力狂潮；一边是垂柳枝头悬挂的冰柱，一边是形式化证明的纯粹符号；一边是 AI 在纯数字空间里生成定理，一边是我刚刚用双手擦净的窗台、搬开的纸箱、摆正的样品。

我戴上耳机，听了一遍希尔伯特 1930 年柯尼斯堡电台讲话的录音。那个苍老而坚定的声音说出那句跨越百年的箴言：“Wir müssen wissen — wir werden wissen.”（我们必须知道，我们终将知道。）

一个试用期外贸业务员，在打扫新办公室的间隙被卷进世纪数学难题的洪流——这三种声音共同指向同一个问题：数学知识，究竟是如何被人类所理解的？它需要身体吗？需要感受吗？需要一双刚擦完地板、还残留着清洁剂气味的手吗？

这个问题，就是这篇文章的起点。

引言：一个词的分量

“理解”——我们每天都在使用这个词，却很少追问它意味着什么。

当一位数学家说“我理解了黎曼猜想”，他说的不是“我知道黎曼猜想的陈述”，也不是“我能够复述它的证明”，更不是“我验证了它在有限情形下的正确性”。他说的是某种更深的东西：他看到了零点的分布与素数计数之间的联系，看到了函数方程如何约束可能的零点位置，看到了整个理论的各个部分如何相互支撑、彼此照亮。这种“看到”，不能被压缩为任何有限的形式规则。

2026 年，当 AI 以流水线方式生成数学证明时，这个词的含义突然变得不再自明。一个 Lean 内核验证通过的证明，不需要任何人理解它。它的合法性来自形式系统的规则，不来自人类心灵的构造。如果数学知识的合法性不再需要“被理解”，那么“理解”在数学中还剩下什么位置？

这就是本文要追问的问题。但在开始之前，我必须先纠正一个错误——一个我在初稿中犯下的、被同行评审准确指出的词源学错误。这个错误本身，恰恰是“理解”之困难的一个绝佳例证。

第一章理解的词源学：历史、隐喻与论证的界限

1.1 一个被修正的词源

在初稿中，我写道：“在英语中，understand 由 under 与 stand 构成。其字面含义是‘站在下方’。”

这个说法是错误的。根据《牛津英语词典》和在线词源词典的记载，古英语 understandan 中的 under 并非来自表示“在下方”的常见词义，而是来自原始印欧语词根 *nter-，意为“在……之间、在……之中”（between, among）。这个 *nter- 正是梵语 antar、拉丁语 inter 的来源。古英语中许多以 under- 开头的复合词都取“在……之中”的含义，例如 underfindan 意为“觉察、探明”。

初稿中还曾断言 under-standan “很可能是希腊语 καταλαμβάνω 的逐词翻译”。这一断言同样缺乏证据：权威词源词典所对举的希腊词是 epistamai（“stand upon”），而非 καταλαμβάνω。有论者作过此类猜想，但要确立“古英语对希腊语的 calque”之说，需要真正的历史语言学证据。因此本文撤下这一断言，只保留词根层面的修正。

1.2 词源不能证明哲学本质

这里必须做出一个关键区分，否则我将在同一篇文章中犯下与初稿同构的错误。

词源学为我们提供了一组关于“理解”的隐喻资源，但它本身不足以决定理解的哲学定义。 即使 under-standan 的一个通行解释确实与“站在事物之中”有关，也不能从“这个词过去可能意味着站在其中”推出“现代理解的本质就是进入对象内部”。词源材料本身的说法是“可能字面意为‘站在中间’”，同时明确说明存在其他解释——它不是已经确定的词源事实。

因此，我需要将词源的哲学地位降低半级：词源不是论证，而是隐喻的源泉。 它提醒我们注意理解的空间性和身体性维度，但不能替我们决定理解的本质。

1.3 三种语言，三种理解姿态——作为隐喻资源

在承认词源不能决定哲学定义的前提下，我们仍然可以考察不同语言中“理解”一词的隐喻结构。

英语的“在……之中”，德语的“站在面前”（vor-stehen：立于事物面前、让事物迎面而立——“对象”的德文 Gegenstand 字面即是“立于对面之物”），法语的“抓住”——三种语言，三种理解姿态。它们共同指向一个更根本的事实：理解不是一种被动的接受，而是一种主动的构造。理解者不是一面镜子，而是一个立法者。

这个洞见，正是康德在《纯粹理性批判》中提出的核心命题。

1.4 从词源到观念：理解作为构造

数学判断是先天综合判断：它们不依赖于经验，却扩展我们的知识。7+5=12，这个命题的谓项“12”并不分析地包含在主项“7+5”之中。要得到 12，我们必须借助直观——康德说的是“纯直观”，即时间与空间这两种感性形式——进行构造。

康德指出，数学认知具有一个区别于其他认知的特征：它必须预先在直观中呈现其概念，而且是在一种非经验的、纯粹先天的直观中呈现，否则它无法前进一步。算术依赖于时间的连续性，几何依赖于空间的延展性。数学之所以可能，是因为人类心灵具有一种先于经验的构造能力。

这里需要两处谨慎。其一，“算术依赖时间”并非《纯粹理性批判》中的明文命题，而是帕森斯（Parsons）、弗里德曼（Friedman）等学者对康德“先验感性论”的通行诠释路径（出处见“注释与出处”）。其二，康德的模型将数学的合法性锚定在人类心灵的构造能力上，但这并不直接推出“只有生物人类才能承担数学构造”。更准确的表述是：康德给出了一个历史上极具影响力的人类主体性模型；AI 迫使我们重新检验这个模型是否必须以人类心灵为唯一承载者。

1.5 意义的累积与理解的动态性

词源学告诉我们，“理解”不是一次性的行为，而是持续的过程。古英语中存在一组以 under- 开头的认知动词——understandan（理解）、underfindan（觉察、探明）、undergitan（领悟）等——它们并存于同一语言中，说明当时的使用者在不断尝试用不同的方式表达“理解”这一概念。

更重要的是，《牛津英语词典》为 understand 列出了数十个义项，其中相当一部分已经废弃（具体数字随版本变动，本文以 OED 网络版 2026 年 10 月条目为参照，请读者以最新版本复核）。这意味着，“理解”的含义本身是在历史中演变的。每一次使用时，它都在被重新定义。

这给了我们一个关键的洞见：数学知识的合法性不仅来自“被构造”，还来自“被共同体重构”。一个证明不会因为被“理解”一次就完成——它需要在不同的语境中被重新理解、重新阐释、重新应用。

第二章数学史上的危机与“理解”的变迁

2.1 第一次数学危机：无理数与“万物皆数”的崩塌

按传统叙述，公元前 5 世纪，毕达哥拉斯学派深信“万物皆数”——宇宙中的一切现象都可以归结为整数或整数之比。然而，学派成员希帕索斯发现，等腰直角三角形的直角边与斜边不可通约：边长为 1 的正方形，其对角线长度 √2 无法用任何整数或分数表示。这一发现直接挑战了“万物皆数”的信条，造成了数学史上的第一次危机。

这里需要注明：“危机”的叙事来自后世数学通史的整理（如克莱因），而希帕索斯传说与“危机”本身的历史性，在史学界存在争议（出处见“注释与出处”）。本文沿用这一叙事，是为了提炼其认识论结构，而非将其当作编年史事实。

这次危机的本质是本体论危机：数学的基础——数本身——被证明无法覆盖几何量。约公元前 370 年，欧多克索斯通过建立比例论，用几何方法处理不可公度量，巧妙地避开无理数这一“逻辑上的丑闻”，将数的概念与量的概念分开。这一理论后被欧几里得收录于《几何原本》，危机得以缓解，但代价是算术长期依附于几何框架发展。

值得注意的是，危机的解决方式不是“发现了无理数的严格定义”（那要等到 19 世纪），而是建立了一套可以容纳不可公度量的新的语言——比例论。这是一次典型的“通过重新表述问题来消解问题”的数学进步。

2.2 第二次数学危机：无穷小的“消失量的鬼魂”

17 世纪，牛顿和莱布尼茨独立建立了微积分算法框架。微积分在物理和工程中取得了惊人成功，但它的基础——无穷小量——从未获得严格的数学定义。1734 年，哲学家贝克莱发表《分析家》，质疑微积分的逻辑严谨性：无穷小量究竟是不是零？如果是零，怎么能用它做除法？如果不是零，为什么最后又被消去？他称导数为“消失量的鬼魂”。

这次危机的本质是认识论危机：数学知识的可靠性依赖于一个无法被严格定义的概念。18 世纪的数学家实际上在一种“操作主义”的立场上使用微积分——只要计算正确，基础问题可以搁置。

直到 19 世纪，波尔查诺和柯西引入极限理论，用严格的逻辑定义了连续性、导数、微分和积分，明确指出无穷小量是一个以零为极限的变量。魏尔斯特拉斯进一步引入“ε-δ”语言严格化极限概念。但柯西之后，魏尔斯特拉斯等人发现，极限的定义会牵涉到实数，而实数仍然是一个未定义概念。实数理论体系的建立（戴德金分割、康托基本序列）才最终完成了这次危机的化解。

第二次危机的解决方式提供了一个关键模式：一个直观上有效但逻辑上不严格的概念，最终通过发明新的形式语言被精确化。无穷小从“鬼魂”变成了“以零为极限的变量”。但这也埋下了一个问题：这个新的形式语言，是否完全捕捉了原始直观中的所有内容？

2.3 第三次数学危机：罗素悖论与基础的裂痕

19 世纪 70 年代，康托创立集合论，为现代数学提供了统一的基础。集合论似乎为数学建立了牢不可破的公理体系大厦。然而，1902 年，罗素在康托的一般集合理论的边缘发现了一个悖论：考虑“所有不包含自身的集合”的集合，这个集合是否包含自身？无论回答是或否，都会导致自相矛盾。罗素用“理发师悖论”做了通俗表述：一个理发师声称他只给那些不给自己理发的人理发，那么他该不该给自己理发？

这次危机的本质是基础性危机：数学最底层的根基——集合论——出现了裂痕。如果集合论出现了矛盾，整个数学大厦都可能摇摇欲坠。

策梅洛率先提出七条公理，建立了没有悖论的集合论；弗伦克尔在其基础上改进，形成了 ZFC 公理系统。但哥德尔不完备定理进一步表明，任何足够强的形式系统都包含不可判定的命题。这意味着，第三次危机并没有被“解决”——它被管理了。数学家学会了在一个经过修补的公理系统中工作，同时承认这个系统有其内在的局限。

2.4 三次危机的模式：每一场危机的解决都在重新定义“理解”

回顾三次危机，一个清晰的模式浮现出来：

	第一次危机	第二次危机	第三次危机
危机类型	本体论	认识论	基础性
核心冲突	数与量不可通约	无穷小无法定义	集合论自指矛盾
解决方式	建立比例论，避开无理数	极限理论，发明ε-δ语言	ZFC公理系统，修补基础
“理解”的变化	从“数即万物”到“几何量优先”	从直观操作到逻辑严格化	从绝对确定性到可管理的局限

注：“危机类型”的本体论/认识论/基础性三分，是本文的解释性框架，而非史学界共识。

每一次危机都迫使我们重新定义“理解”的含义。第一次危机后，理解数学意味着理解几何比例；第二次危机后，理解微积分意味着理解极限的 ε-δ 定义；第三次危机后，理解数学意味着理解一个公理系统的边界。

当前 AI 数学的挑战，正是第四次危机的开端：当形式系统可以独立于人类理解而验证证明时，“理解”在数学知识中是否还有位置？

第三章理解的分层：一个概念框架及其可观测判据

3.1 六个层次的理解

在进入 AI 数学的讨论之前，我必须先建立一个概念框架。因为初稿最大的问题，正如审稿人所指出的，是我把“人类的结构性理解”偷偷提升为“理解本身”，然后据此证明 AI 缺乏理解。这是一个循环论证。

为了避免这个陷阱，我需要把“理解”拆分为至少六个维度，并且为每一层给出可观测判据——即什么样的行为表现可以指示这一层次的理解正在发生。

第一，句法理解：知道一个证明的形式结构，能够识别它的符号、规则和推导步骤。可观测判据：能够正确解析（parse）一段形式化代码，识别其语法结构，区分合法与不合法的表达式。一个能够解析 Lean 代码的机器具有句法理解。

第二，验证性理解：能够确认一个推导在给定规则下是否合法。可观测判据：能够执行内核检查（kernel check），对给定的形式化命题和证明，判断其是否满足形式系统的推导规则。Lean 内核具有形式验证能力。本文约定：“验证性理解”专指对推导合法性的确认，“内核检查”则指 Lean 等系统执行这一确认的技术机制，两者不混用。

第三，操作性理解：能够运行、修改、迁移一个证明。可观测判据：能够修复（proof repair）一个失败的形式化证明，能够将证明从一个数学语境移植（porting）到另一个语境，能够替换引理、调整参数、简化步骤。一个熟练的数学使用者具有操作性理解。

第四，解释性理解：能够解释一个证明为什么成立。不是“它成立”，而是“它为什么成立”。可观测判据：能够回答针对证明动机的反事实提问——“若去掉引理 X，这一步为何失效？”“若更换假设 Y，结论如何改变？”——或给出一个独立可检验的简化证明，使人类评审者无需逐行核查即可把握其核心思想。

第五，结构性理解：能够看到证明在更大理论图景中的位置。可观测判据：能够构建定理图谱（theorem graph），识别证明与其他结果的相关性，定位其在数学知识网络中的节点，进行抽象（abstraction）和推广。但需承认：这一层的即时行为判据，与“模式匹配”难以截然区分（见第七章反对五）。

第六，生成性理解：能够利用结构性理解创造新的结果。可观测判据：提出新猜想（novel conjecture）、发现新概念、建立新框架、开辟新领域。但同样需承认：这一层的可靠判据可能只能是历史性的——其产物是否被共同体后续采用、推广与吸收，而非任何即时的行为表现。这一承认不是框架的缺陷，反而将第五、六层与第八章的共同体规范化主线焊接在一起。

这六个层次不是等级森严的阶梯，而是一个光谱。一个数学家可能在不同层次上有不同的能力。一个 AI 系统也可能在不同层次上有不同的表现。顺带说明：教育心理学中斯克姆普（Skemp, 1976）关于“关系性理解”与“工具性理解”的经典区分，与本文第二层以上与第四层以下的划分遥相呼应；但本文框架面向的是数学知识的生产与规范化，而非课堂学习。

3.2 这个框架的用途

有了这个框架，我们就可以问出更精确的问题：

当前的 AI 系统在哪几个层次上具有理解？
形式化验证在哪几个层次上提供了保证？
数学知识的合法性需要哪几个层次的理解？

修正后的说法是：

当前的 AI 系统在句法理解和形式验证能力上表现优异，在操作性理解上正在快速进步，但在解释性理解、结构性理解和生成性理解上，其能力仍然有限，且其局限性不是技术性的，而是认识论性的。

更精确的统一立场是：当前 AI 系统在结构性理解与生成性理解上缺乏充分证据，且其缺口是认识论性质而非算力性质；至于这一缺口是否原则上不可逾越，本文悬置——既不武断宣称“人类独有”，也不轻率断言“指日可待”。

这个说法既不过强，也不过弱。它承认 AI 的能力，同时指出其局限。更重要的是，它把争论从“AI 有没有理解”转移到了“AI 在哪些层次上有理解，这些层次是否足以构成数学知识”。

3.3 形式正确性、理解与知识

现在我们可以做出三个关键区分：

形式正确性 ≠ 理解 ≠ 数学知识

形式正确性是一个技术概念：一个推导在给定形式系统下是否合法。Lean 内核可以判定形式正确性。

理解是一个认识论概念：一个主体是否把握了证明的结构、意义和位置。理解是多层次的，不能被还原为形式正确性。

数学知识是一个共同体概念：一个结果是否被数学共同体接受为知识。数学知识不仅要求形式正确性，还要求共同体对其意义的把握、对其位置的定位、对其价值的认可。

这里需要更精细地区分三个词：真理（truth）、知识（knowledge）、知识共同体中的规范化（canonization）。

层次	概念	裁决者
真理	命题为真	世界
知识	被证明，且被理解	认知者
规范化	被共同体接受为可传承的知识	数学共同体

一个命题可以是真的，但未被证明。它可以被证明，但未被理解。它可以被理解，但未被共同体接受。它可以被共同体接受，但未被理解。这些区分是本文的核心框架。

更重要的是，它允许我们避免两个极端：既不说“AI 不能做数学”，也不说“AI 已经理解了数学”。

3.4 方法论说明：具身性在本文论证中的位置

在进入第四章之前，需要说明一个方法论问题，以免读者误读全文的论证结构。

本文标题中的“具身”，需要被精确地定位。第四章将讨论具身现象学与具身认知科学，但它们的论证地位如下：具身性是解释“人类理解何以可能”的候选机制，而不是裁决“AI 能否理解”的充分或必要条件（§4.3 将给出科学层面的降调）。换言之，第四章的功能是回答“人类的理解碰巧是具身的，这告诉我们什么”，而不是回答“没有身体就必然不能理解”。

因此，真正承担本文论证重量的，不是具身性，而是第三章的六层区分与 3.3 的三重区分（真理/知识/规范化），以及第五章、第八章展开的共同体认识论立场：数学知识的合法性，最终锚定在“共同体意义上的理解”。结论章会回到这一点。具身性在本文中的角色，是让“理解需要共同体的在场、倾听与回应”这一抽象命题获得现象学上的厚度——它提供叙事，不提供判决。

这一说明的代价，是承认标题的“具身”二字更多是对人类理解现象的命名，而非对 AI 理解可能性的否定论证。我认为这是诚实的代价，值得支付。

第四章具身理解的哲学根基：作为候选机制，而非必要条件

4.1 胡塞尔：数学对象的现象学构成

在格罗滕迪克之前半个世纪，埃德蒙德·胡塞尔已经从另一个方向触及了同一个问题。

胡塞尔在《算术哲学》（1891；Husserliana 第 XII 卷）中提出，数的概念不能被逻辑地定义。他写道：“困难在于现象，在于对现象的正确描述、分析和解释。只有参照现象，才能获得对数概念本质的洞见。”对胡塞尔来说，体验数学对象和体验物理对象在原则上没有区别——两者都是意识活动所构成的对象。

胡塞尔的本质直观，与康德的经验直观不同。康德认为人类只能直观现象，不能直观物自体。胡塞尔则认为，本质本身就是可直观的。当我们看一个红色的三角形，我们不仅看到这个具体的红色和具体的三角形，我们还看到“红色”和“三角形”的本质。以集合关系为特征的数不是源自我们不可直觉到的外部对象中的内在性质，而是在本质上归结为作为一种特殊“意识样式”的意识的高阶活动。

这里需要明确一个学术上的谨慎：早期《算术哲学》的心理主义/现象学尝试与后期超越论现象学关于理想对象、语言、历史性、主体间性的论述，不能简单当成同一个理论版本。 本文并非主张早期胡塞尔已经提出今天意义上的具身认知理论，而是说，他的现象学工作为后来从经验、主体间性和理想对象构成的角度理解数学提供了一条思想谱系。

胡塞尔在其晚期手稿《几何学的起源》（1936，作为《欧洲科学的危机》附录三发表）中提出了一个关键概念：语言是几何学的 Sprachleib（语言身体）。这意味着数学真理不能脱离其语言和符号的具身化而存在。

4.2 梅洛-庞蒂：数学的具身认知与运动意向性

梅洛-庞蒂对数学认知的具身-生成解读，是当前数学哲学中最具原创性的欧陆哲学贡献之一。

他的核心主张是：数学认知不仅需要具体可感知符号的在场和实际操作，更根本地，它关联于符号系统的具体构型的结构性转换，而这些结构性转换是通过运动意向性来操作的。

在梅洛-庞蒂看来，数学对象是关系性实体——即格式塔，这些格式塔必然蕴含处于情境中的认知者，认知者与它们在世界中建立特定类型的互动，而数学对象在其最终的结构性转换中依赖于这些认知者。这意味着，数学理解不是一种脱离身体的纯粹智力活动，而是一种身体化的实践——通过手势、操作、空间运动来把握数学结构。

这里需要明确：这是本文对梅洛-庞蒂的二级解释，而非直接引述。 我们将其身体主体、格式塔与运动意向性的概念框架，理解为对数学认知的一种现象学描述，而不是让梅洛-庞蒂背负一套完整的数学本体论。

4.3 具身认知科学的实证证据：支持机制，而非必要条件

具身认知理论强调身体与环境的交互对所有形式的学习（包括数学）都至关重要。实证研究表明，认知是具身的，即使在通常被认为是“抽象”的高级数学推理领域也是如此。

基于学习者与教师的手势研究提供了直接证据。研究表明，数学知识是具身的——表征性手势展现了行动和感知的心理模拟，而一些隐喻性手势反映了基于身体的概念隐喻。手势涉及数学意义建构时，比纯粹的图标手势在时间上更延展、在结构上更有组织（Goldin-Meadow 2003；Alibali & Nathan 2012；Novack & Goldin-Meadow 2015；Abrahamson & Bakker 2016；详见“注释与出处”）。

运动、手势和具身行动在数学概念加工中扮演着核心角色。

然而，这里必须做出一个关键的科学判断。 现有具身数学认知研究确实支持：身体、动作、手势、感知环境会参与数学认知，并能促进某些数学学习和推理；近年来的综述也总结了手势对数学学习、迁移和保持的积极作用。但这并没有证明：没有身体 → 就不可能产生数学理解。

更准确地说，行动可以促进洞见，但单独的行动并不足以产生有效的证明，还需要与语言系统结合。

因此，科学上更安全的结论是：

具身性可能是人类数学理解的重要认知支撑机制之一，但尚不能据此推出具身性是数学理解的普遍必要条件。

这个结论与本文的立场并不冲突，反而更精确。我们真正应该攻击的不是“AI 没有身体，所以 AI 不可能理解数学”，而是“现有 AI 数学系统尚没有充分证据表明，它获得了与人类数学理解相当的概念性、情境性和生成性结构”。

4.4 格罗滕迪克：结构性理解的案例

在二十世纪后半叶，亚历山大·格罗滕迪克用他的一生给出了另一种回答。

格罗滕迪克的伟大不在于他证明了多少定理。他的伟大在于他重新定义了数学是什么。在他的回忆录《收获与播种》中，格罗滕迪克写道，构成他研究的本质与威力的，不是成果或大定理，而是“观念，甚至梦想”。

他的核心概念“Motive”，被他描述为“终极上同调不变量”，所有其他的上同调理论都是它的“实现”或“化身”。有中文论者将这一纲领比作“佛”与“化身”的关系——需要注明：这是二手阐发，并非格罗滕迪克本人的表述。我们真正要抓住的不是技术性的 motive 定义，而是概念的统一能力。

这里需要做出一个重要的降调：格罗滕迪克的 motive 纲领试图寻找一种能够统一不同上同调实现的更深层结构，而不是一个已经被完全定义清楚的终极对象。

格罗滕迪克的数学风格，用他自己的话说，是“异常自然”的。他不追求技巧的精妙，而是追问：什么是最自然的构造？什么概念一旦被正确地表述，整个问题就自动解决？

这里需要谨慎。我们无法断言格罗滕迪克“知道”理解是不可形式化的。更严谨的表述是：从格罗滕迪克的数学实践中，我们可以看到一种与形式证明不同的结构性理解。 这种理解的特征是：它追问的不是“这个推导是否合法”，而是“什么是最自然的构造”；它追求的不是技巧的精妙，而是概念的自然性；它把握的不是孤立的证明，而是证明在理论网络中的位置。

第五章计算认识论：认知脚手架与理解的重新分工

5.1 延展心智与认知脚手架

在之前的讨论中，我们一直在“人类理解 vs. 机器验证”的二元框架中思考。但这个框架本身可能需要被超越。

安迪·克拉克和大卫·查尔默斯在 1998 年提出的“延展心智”理论，为我们提供了一个全新的视角：认知过程并不局限于颅骨之内。当我们用纸笔计算乘法时，纸和笔不仅是认知的因果辅助工具，而是认知过程的构成部分。数字被外部表征、操作和存储，纸笔承担了短期记忆的功能，因此应当被赋予认知地位。

这一理论对数学认知有直接的启示。数学知识既需要程序性流畅，也需要概念性知识。使用外部资源可以让人们调用他们的概念性知识，从而增强整体的数学流畅性。

Lean 不应被视为剥夺人类理解的异己机器，而应被视为人类数学家心智的“外脑”和“认知脚手架”。 正如纸笔扩展了人类的计算能力，Lean 扩展了人类的验证能力。

5.2 形式化作为公共语言

这一视角的转变至关重要。对于彼得·舒尔茨等发起“液态张量实验”的顶尖数学家（该实验的形式化工作由 Commelin 等主导）以及陶哲轩（其 Lean 实践主要见于 PFR 等项目）而言，形式化并非“不透明的机器输出”，而是一种消除人类直觉歧义的、更严苛的“公共语言”。

Lean 社区的发展证实了这一点。Mathlib 的持续增长表明，形式化数学正在成为一种活的语言。Verbose Lean 库被用于教学，帮助学生读写传统纸笔证明——Lean 证明看起来像自然语言，因此容易迁移到纸上。这恰恰说明，形式化不是理解的对立面，而是理解的“压力测试”。

一个数学定理，当它被形式化时，它所有的隐含假设都被显式化了。那些人类数学家“默契地知道”的条件，那些“显然”的推导，都被要求明确给出。这不是理解的剥夺，而是理解的精确化。

5.3 两种理解的互补与一个未解决的问题

基于延展心智和认知脚手架的理论框架，我们可以提出一个关键区分：

验证性理解：理解一个证明的每一步推导是否合法。这是 Lean 内核可以完成的。

结构性理解：理解一个证明为什么重要、它的核心思想是什么、它可以推广到哪里。这是人类数学家目前独有的——但这里的“目前”是一个经验判断，而非概念断言：AI 在结构性理解上缺乏充分证据，其缺口是认识论性质而非算力性质，是否原则上不可逾越，本文悬置（见 3.2 与第七章反对五）。

AI 可以加速验证性理解，从而将人类数学家的认知资源解放出来，去进行结构性理解。这不是“理解的终结”，而是理解的重新分工。

但这引出了一个尖锐的问题：如果认知本来就可以延展，那么为什么 AI 参与的认知过程仍然不能算理解？

如果人类认知 + 纸笔 = 认知过程，那么为什么人类认知 + AI + Lean ≠ 认知过程？

这个问题的回答需要区分“认知过程的构成”与“认知主体的构成”。纸笔是认知过程的构成部分，但纸笔本身不是认知主体。它不提出假设，不做出判断，不承担责任。认知哲学家对“耦合不等于构成”已有系统的论证：延展认知的批评者（Adams & Aizawa 2008）提醒我们，判断一个系统是否具有心灵，要看它是否具有“认知标志”（the mark of the cognitive）；纸笔与人体耦合，并不因此构成心灵。

AI 则不同。一个 AI 系统可以生成证明、提出猜想、修正错误。它在某种程度上表现得像一个认知主体。但这不意味着它就是一个认知主体。

一个 AI 系统是否能够成为认知主体，取决于它是否能够：对自己的输出负责；对自己的错误进行反思；对自己的推理进行解释；与人类进行真正的对话。

当前的 AI 系统在这些方面仍然有限。它不“在场”。它不“倾听”。它不“回应”。它只是生成输出。

但这不意味着 AI 永远不能成为认知主体。也许未来的 AI 系统可以获得这些能力。如果那一天到来，那么“人机混合数学共同体”就不再是一个隐喻，而是一个现实。

5.4 人机混合数学共同体

如果接受这一框架，那么 AI 数学的未来不是“人类理解 vs. 机器验证”的零和博弈，而是人机混合数学共同体的构建。

在这个共同体中，机器负责底层的、繁琐的验证性理解；人类负责高阶的、创造性的结构性理解。机器生成的证明经过形式化验证后，由人类数学家进行阐释、接受和规范化。人类的直觉和创造力被引导向“提出好问题”，而机器被引导向“验证和探索”。

但这需要一个前提：认识论规范的建立。未来的数学奠基，不仅在于人类如何理解数学，更在于人类如何建立一套规范，去审查、解释并同化机器生成的“非直观真理”。这套规范必须解决以下问题：

认证标准：一个 AI 生成的证明，需要满足什么条件才能被数学共同体接受为知识？
可读性要求：AI 生成的证明是否需要满足最低限度的可读性标准？
独立验证：如何确保 AI 生成证明的验证独立于生成方？
知识传承：AI 生成的知识如何被纳入数学教育和学徒制？

这些问题没有现成的答案。但它们定义了“数学的危与机”的真正含义。

第六章 AI 数学的现状：形式验证与语义忠实

6.1 OpenAI 722 篇手稿：流水线时代的来临

截至 2026 年 10 月 7 日，OpenAI 发布了一批数学成果（openai/math 仓库）：722 份论文或相关手稿，对应 372 组数学结果，覆盖数论、几何、数学物理等 17 个领域，共测试约 4,000 个问题。其中，仓库声称给出了有理数域上希尔伯特第十问题（H10/ℚ）的否定性解决——注意：这是“声称”，未经独立验证；并覆盖准黎曼假设方向（ζ 与 Dirichlet L-函数在 Re s > 7/8 的零自由区域），而非黎曼猜想本身。部分成果提供了 Lean 形式化证明，但许多手稿仍缺乏形式化的 Lean 版本。OpenAI 明言，未经 Lean 形式化的结果“可能会有问题”。

这次发布的核心特征不是“AI 解决了难题”，而是**“AI 以工业化方式生产数学证明”**。平均每个结果消耗约等于 ChatGPT Pro 连续思考 3 小时的算力。这不是一次性的“灵感爆发”，而是一个可复制、可规模化的生产管线。

这里需要明确：“工业化方式生产数学证明”是本文的解释性判断，而非 OpenAI 的官方自我定义。OpenAI 的公开仓库确实写明其绝大多数结果采用相同程序、由内部模型产生、平均每个结果使用约三小时 ChatGPT Pro thinking compute。但将其称为“工业化”，是作者对这一生产模式的概括。

6.2 独立复核的发现：kernel soundness ≠ semantic faithfulness

截至 2026 年 10 月 7 日，第三方复核者的公开记录显示：OpenAI 的自家 Lean 验证断言和公开形式化元数据，“不能替代第三方、哈希锁定、exit-0 的内核证书”。在锁定的 OpenAI commit 上，Comparator 已重建相关提交，Lean 默认内核和 nanoda 都接受了提交的定理，并确认其符合 Comparator 的目标命题；不过，完整仓库的独立默认 lake build 仍是另一个尚未完成的 gate。换言之，独立复核的方向一致：局部形式化成立，整体独立复现未完成。以上进展属于移动靶，具体表述需对应到可引用的 commit 与存档快照（见“注释与出处”）。

更关键的是 Navier–Stokes 案例。2026 年 10 月 6 日，Bastounis、Circelli 与 Hansen 的论文（arXiv:2610.08144）直接讨论“NL → Lean”的语义对应问题，主张 OpenAI 的 Navier–Stokes Lean 形式化与自然语言的爆破（blow-up）证明并不对应。这里需要补一个常被忽略的技术细节：OpenAI 的结果是带光滑外力的爆破，对应克雷千禧问题官方表述中的 C/D 选项；无外力情形的 A/B 选项并未解决。这一区分，正是“语义忠实性”争论的实质背景。

这恰恰使问题变得更加精准：问题不再是“Lean 有没有通过”。问题是：Lean 到底验证了哪个被形式化的命题？它与原始数学主张之间的语义映射是否可靠？

这可以成为全文非常漂亮的一条主线：kernel soundness ≠ semantic faithfulness。形式化内核的可靠性，不等于自然语言数学主张与形式化命题之间的语义忠实性。

6.3 25 位菲尔兹奖得主的联署声明

2026 年 9 月 11 日，25 位菲尔兹奖得主联合发表声明《人工智能在数学中的严重错位》（mathandai.org；签署者包括陶哲轩、邓煜、舒尔茨等），批评 AI 公司把解决数学难题当作模型能力的基准测试。声明指出，AI 公司的目标（跑分）和数学共同体的目标（理解）之间发生了系统性错位，并批评这类成果“被匆忙宣布，没有留出规范写作的时间”。

这不是学术竞争，这是叙事竞争。当 AI 公司在社交媒体上每隔几天就宣布一次“突破”时，数学家的反应不是兴奋，而是“应接不暇”。

声明明确把“problem solving”与“conceptual understanding and insight”区分开来，并强调数学知识需要经过讨论、写作、简化、传承才能进入数学共同体的长期知识体系。这与本文的核心框架高度共振。

6.4 神谕机与祭司

图灵在 1939 年的《基于序数的逻辑系统》中提出了“神谕机”（o-machine）的概念：一台带有黑盒的图灵机，它能在一步之内回答任何无法计算的问题。

这里需要说明类比的限度：神谕机是直接回答不可计算问题的理论装置；而 Lean 验证通过的证明是可计算的推导链，人类数学家原则上可以逐行核查它。 AI 证明生成器带来的问题不是“神谕性”，而是不透明性与不可消化性——不是不能查，而是查不过来、查了也不产生理解。这一区分，与蒂莫茨科（Tymoczko）在四色定理争论中提出的 surveyability（可综览性）概念直接相关（见第七章反对二）。

今天，AI for Math 正在把数学家变成人肉“神谕机”的终端。当 AI 用流水线生成成百上千页、跨越几十个新定义的 Lean 代码时，人类数学家的大脑带宽将瞬间被撑爆。面对一个机器验证通过、但完全无法“人脑消化”的定理，数学家面临两个选择：拒绝接受，或承认它是“定理”，并成为这台神谕机的“祭司”。

于是，数学界的工作模式将发生极其荒诞的异化：数学家不再去理解数学，而是去宣告数学。他们站在讲台上，对着满堂的学生说：“根据神谕机（AI）的验证，这个命题是真的。为什么？不知道，但 Lean 内核证明了它。”

如果数学共同体把可验证性逐渐当作理解的替代品，数学知识生产可能发生一种深刻的异化。 这不是“数学知识就死了”的修辞宣判，而是一个可讨论的命题。

第七章反对意见与回应

反对一：形式正确性本身就是知识

一个形式主义者会问：为什么需要“理解”？只要证明正确，数学知识就成立。

回应：这个反对意见预设了一个特定的知识概念——知识就是被证明的真命题。如果数学知识就是被证明的真命题，那么数学史的大部分内容——概念的发明、框架的建立、问题的提出——都不算知识。这显然是一个过窄的知识概念。更合理的知识概念应该包含理解。一个证明不仅需要正确，还需要被理解、被阐释、被定位。

反对二：人类数学家也大量依赖不可理解的形式结构

如果人类可以接受极其冗长的计算机辅助证明，为什么 AI 生成就必须特殊处理？

回应：四色定理的证明从未被任何人完整阅读过。但人类数学家接受它，是因为它的核心思想——不可避免集和可约构型——被共同体理解了。这正是蒂莫茨科（Tymoczko, 1979）在四色定理哲学论战中提出的 surveyability（可综览性）问题：计算机辅助证明若不可被人类综览，其认识论地位就需要重新界定——围绕这一点的争论至今未息（Burge、Detlefsen & Luker、McEvoy 的后续文献见“注释与出处”）。AI 生成的证明缺少的，正是这种可被共同体消化的结构。

反对三：你是否把“理解”拟人化？

也许 AI 根本不需要拥有人的理解方式。

回应：数学知识的合法性来自数学共同体的接受，而数学共同体是人类共同体。这里需要说明：这是一个关于当前事实的断言，而非概念真理；本文的规范主张是条件式的——只要数学共同体由人类构成，理解标准就内嵌于人类实践。如果 AI 有一种完全不同的理解方式，这种理解方式是否能够被人类共同体接受？当前 AI 的“理解”方式与人类共同体的理解方式之间存在巨大的鸿沟。

反对四：共同体接受并不是知识的充分条件

数学共同体可能集体犯错。

回应：共同体接受不是知识的充分条件，但它是数学知识共同体稳定化/规范化的条件。一个结果如果不被共同体接受，它可能仍然是正确的数学知识，但尚未成为共同体意义上稳定、可传承、可引用的数学知识。

反对五：AI 可能最终获得结构性理解

如果 AI 可以发现概念、提出猜想、证明猜想、找到反例、解释证明、迁移理论、创造新的数学语言，那么“AI 没有结构性理解”还能成立吗？

回应：这个反对意见是开放的。如果 AI 真的能够做到这些，那么它确实具有结构性理解。但当前的 AI 系统在这些方面仍然有限。它可以在有限程度上发现概念、提出猜想、找到反例，但它的“解释”往往是事后合理化的，它的“迁移”往往是模式匹配的，它的“创造”往往是组合性的。

这不意味着 AI 永远不能获得结构性理解。也许未来的 AI 系统可以获得。如果那一天到来，那么本文的论证就需要修正。但在此之前，我们需要保持谨慎：不要因为 AI 可以生成形式正确的证明，就认为它已经理解了数学。

第八章数学的危与机

8.1 危：理解的边缘化

现在，我们可以回到最初的问题：数学的危与机。

数学的危机不在于 AI 做数学，而在于我们忘记了数学不只是做数学。 当证明生成的成本趋近于零，数学共同体面临一个选择：是接受 AI 的输出作为数学知识，还是坚持数学知识必须经过共同体的理解。

如果数学知识的合法性不再来自“被共同体理解和接受”，而是来自“通过内核检查”，那么数学就不再是人类的知识，而是机器的输出。这不是一个技术问题，而是一个认识论问题。

一个无人能读的证明，算不算数学知识？

瑟斯顿在 1994 年已经回答过这个问题。他说，数学进步的形式包括“理解已有结果”，而理解不是一次性的——它是持续的、动态的、共同体性的。一个证明不是被“理解”一次就完成了，它需要在不同的语境中被重新理解、重新阐释、重新应用。

AI 生成的证明缺少的，正是这种可被重新理解的结构。它可能包含所有必要的推导步骤，但它不包含“为什么这样做是自然的”“这个技巧可以推广到哪里”“这个结果在更大的图景中意味着什么”。这些东西不在形式证明里，它们在数学共同体的对话中。

8.2 机：理解的重新分工

数学的机会不在于 AI 能解决多少难题，而在于它迫使我们重新回答一个被遗忘了很久的问题：数学到底是关于什么的？

AI 使数学第一次能够把验证、搜索、实验、形式化、反例发现大规模外包给机器，从而迫使人类数学把稀缺资源集中到概念选择、结构发现、问题形成和意义解释上。这正是第五章所说的“理解的重新分工”：机器负责验证性理解，人类负责结构性理解，机器生成的证明经形式化验证后，由人类数学家进行阐释、接受和规范化。

这个重新分工需要新的制度。当 AI 可以生成大量证明时，共同体的瓶颈从“生成”转移到“消化”。这意味着我们需要新的制度——新的期刊形式、新的评审流程、新的教育模式——来加速知识的消化和传承。

8.3 研究者永不失去信念

希尔伯特在 1900 年巴黎国际数学家大会的讲演《数学问题》中说：“每一个数学问题都可以被解决，这种信念是对研究者的一种强大激励。”这句话在今天仍然有效，但它需要我们重新赋予它内容。

“知道”不是“验证通过”。“知道”是“理解”。而理解，按照修正后的词源学——作为隐喻资源而非论证——是“站在事物之中”：不是站在被理解者的下方承受它的重量，也不是站在远方审视它，而是进入它的内部，与它共处，在它与其他事物的关系网络中把握它的结构。

数学的未来不是人类与 AI 的竞争，也不是人类对 AI 的依赖。它是人类与 AI 的共同理解——一种新的交互主体性，一种新的数学共同体。

这个共同体不会自动到来。它需要有人去奠基。

8.4 解放思想，实事求是

解放思想，意味着不把任何数学形式——无论是人类证明还是 AI 证明——当作绝对权威。康德的洞见是：数学的合法性来自人类心灵的构造能力。如果我们把这个能力让渡给机器，数学就失去了它的根基。但这不意味着我们拒绝机器。它意味着我们在与机器的互动中重新激活我们的构造能力。

实事求是，意味着坚持数学知识的可理解性、可交流性、可修正性。一个证明，无论它是由人还是由机器生成的，只有在被共同体理解、讨论、修正之后，才成为数学知识。这里的“实事求是”被用作一条实践认识论命题：认知的最终裁决标准，是共同体可参与的实践，而不是任何单一权威。

我们必须知道，我们终将知道。 希尔伯特的话在今天仍然有效。但“知道”需要我们重新定义。它不是“验证通过”。它是“理解”。

数学的危机不在于 AI 做数学，而在于我们忘记了数学不只是做数学。

数学的机会不在于 AI 能解决多少难题，而在于它迫使我们重新回答一个被遗忘了很久的问题：数学到底是关于什么的？

瑟斯顿的答案是关于理解的。格罗滕迪克的答案是关于结构的。哈代的答案是关于美与严肃性的。康德的答案是关于人类心灵的构造能力的。

我的答案是：数学是关于人类共同体如何理解世界的。当这个共同体被算力资本分割成“生成方”和“消费方”时，数学就失去了它最根本的东西。

不是定理，不是证明，不是论文，是理解本身。

后记

在撰写本文的过程中，我犯了一个词源学错误，并被同行评审准确指出。这个错误本身就是“理解”之困难的绝佳例证：我以为我理解了 understand，但我没有去核查它的词源。我以为“站在下方”是一个深刻的洞见，但它是一个虚构的洞见。

这个故事告诉我们：理解需要谦卑。它需要我们去核查、去追问、去修正。它需要共同体的监督。它需要时间。

AI 生成的证明缺少的，正是这种谦卑。它不核查自己，不追问自己，不修正自己。它是一个封闭的系统，而不是一个开放的对话。

但人类共同体也可能缺少谦卑。当我们把 AI 生成的证明当作“验证通过”就接受时，我们也在放弃核查、追问和修正的责任。

理解的奠基，从谦卑开始。

而谦卑，按照修正后的词源学，不是站在下方承受重压，而是站在事物之中，承认自己不知道，愿意去核查、去追问、去修正。

这就是理解的真正含义。

路漫漫其修远兮，吾将上下而求索。 ——屈原《离骚》

作者：良之日期：2026 年 10 月 7 日

本文写作过程中使用了 AI 辅助文献检索与事实核查。文中涉及 2026 年 9—10 月事件的陈述均以“截至 2026 年 10 月 7 日”的公开信息为准，并附可存档来源（见“注释与出处”）。初稿中的词源学错误已经修正，特此说明。

注释与出处

事实性来源（截至 2026 年 10 月 7 日）

OpenAI 数学成果发布：openai/math 仓库（GitHub）及官方博客——722 份手稿、372 组结果、17 个领域、约 4,000 个测试问题、平均每个结果约等于 ChatGPT Pro 三小时思考算力。
H10/ℚ 手稿：同上仓库（“声称给出否定性解决”，未经独立验证）。
准黎曼假设：同上仓库（ζ 与 Dirichlet L-函数在 Re s > 7/8 的零自由区域）。
25 位菲尔兹奖得主联合声明：《人工智能在数学中的严重错位》，2026 年 9 月 11 日，mathandai.org；签署者含陶哲轩、邓煜、舒尔茨等。
Bastounis, A., Circelli, F., & Hansen, A. C.（2026 年 10 月 6 日）：arXiv:2610.08144（Navier–Stokes “NL → Lean”语义对应问题）。
独立复核进展：第三方复核者的公开 checkpoint 记录（Comparator 重建、Lean 默认内核与 nanoda 接受、完整独立 lake build 未完成）——以所引 commit 与存档快照为准。
克雷千禧问题 Navier–Stokes 官方表述（A–D 选项划分），克雷数学研究所网站。

词源学

《牛津英语词典》（OED）understand 条目（网络版，2026 年 10 月查阅；义项数字随版本变动）。
在线词源词典（Etymonline）understand 条目——其表述本身带有保留（“probably…”“the suggestion in Barnhart…”）。
古英语复合动词 understandan / underfindan / undergitan：可查 Bosworth–Toller《盎格鲁-撒克逊词典》。

哲学与数学史文献

康德：《纯粹理性批判》。“算术依赖时间”的解读见 Parsons, C., “Arithmetic and the Categories”（1992）；Friedman, M., Kant and the Exact Sciences（1992）。
胡塞尔：《算术哲学》（1891；Husserliana Bd. XII）；《几何学的起源》（1936；《欧洲科学的危机》附录三）。
梅洛-庞蒂：《知觉现象学》（1945）。本文对其数学认知的论述为二级解释。
格罗滕迪克：《收获与播种》（Récoltes et Semailles）。“佛性/化身”之比为中文二手阐发，非格罗滕迪克本人表述。
希帕索斯与“第一次数学危机”叙事：Kline, M., Mathematical Thought from Ancient to Modern Times（1972）；史学批评见 Knorr, W. R., The Evolution of the Euclidean Elements（1975）及后续研究。
希尔伯特：《数学问题》（1900 年巴黎国际数学家大会讲演）；1930 年柯尼斯堡电台讲演（“Wir müssen wissen, wir werden wissen”）。
Thurston, W., “On Proof and Progress in Mathematics”, Bulletin of the American Mathematical Society, 30(2), 1994.
Turing, A. M., “Systems of Logic Based on Ordinals”（1939）。
Tymoczko, T., “The Four-Color Problem and Its Philosophical Significance”, Journal of Philosophy, 76(2), 1979；后续争论见 Burge（1998）、Detlefsen & Luker（1980）、McEvoy（2013）。
Lakatos, I., Proofs and Refutations（1976）。
Avigad, J., “Understanding Proofs”, in Mancosu (ed.), The Philosophy of Mathematical Practice（2008）。
De Toffoli, S., & Giardino, V., “Forms and Roles of Diagrams in Knot Theory”, Erkenntnis, 79, 2014——图示与具身数学实践。
Corfield, D., Towards a Philosophy of Real Mathematics（2003）。
Clark, A., & Chalmers, D., “The Extended Mind”, Analysis, 58(1), 1998；批评见 Adams, F., & Aizawa, K., The Bounds of Cognition（2008）。
“理解”的认识论：de Regt, H., Understanding Scientific Understanding（2017）；Grimm、Kvanvig、Elgin 的相关讨论。
Skemp, R., “Relational Understanding and Instrumental Understanding”, Mathematics Teaching, 77, 1976。
手势与具身数学认知：Goldin-Meadow, S., Hearing Gesture（2003）；Alibali, M. W., & Nathan, M. J., “Embodiment in Mathematics Teaching and Learning”（2012）；Novack, M., & Goldin-Meadow, S., “Learning from Gesture”（2015）；Abrahamson, D., & Bakker, A., “Making Sense of Movement in Embodied Design for Mathematics Learning”（2016）。
毛泽东自述引文：《西行漫记》（Red Star Over China，埃德加·斯诺，1937）中译本相关章节。