1. 从“辅助”到“重启”：AI如何重塑数学研究的底层逻辑
最近，陶哲轩教授关于AI“重启”千年数学规则的提法，在数学和计算机科学交叉领域激起了不小的波澜。这远不止是“又一个AI工具”那么简单。作为一名长期关注形式化验证与自动化推理的从业者，我深切感受到，我们正站在一个范式转移的临界点上。过去，无论是数学家还是计算机科学家，都默认数学证明是一项纯粹的人类智力活动，其严谨性由同行评议这一社会性过程来保证。而AI，尤其是基于大语言模型和交互式定理证明器的系统，正在将证明本身转化为一种可计算、可验证、甚至可“生长”的对象。
这解决的，是数学研究中最古老也最核心的痛点：信任与复杂性的矛盾。一个数学证明，随着其链条的延长和分支的增多，其正确性验证的难度呈指数级增长。历史上，长达数百页的证明（如有限单群分类、费马大定理的证明）需要顶尖专家团队耗费数年时间进行审阅，其过程本身就可能存在疏漏。AI驱动的形式化验证，如Lean、Coq、Isabelle等工具，提供了一条截然不同的路径：它将数学陈述和证明步骤，编码为机器可严格检查的代码。这意味着，一旦一个证明被形式化并验证通过，其正确性就是绝对的、无需置疑的，其复杂度由计算机的算力来承担，而非人脑的持续专注力。
那么，这个“重启”具体适合谁？我认为有三类人最应该关注：一是前沿的数学研究者，尤其是那些工作在证明极其复杂领域的学者，AI可以作为永不疲倦的“合作者”和“校验员”；二是计算机科学中从事程序验证、安全关键系统开发的工程师，数学形式化的思想与工具正直接应用于确保软件与硬件的绝对正确；三是所有对“知识”的可靠构建与传承感兴趣的人，这或许是人类首次有机会建立一个所有细节都经得起永恒检验的知识大厦。接下来，我将结合具体的技术栈和实操案例，拆解这场“重启”是如何发生的，以及我们如何参与其中。
2. 核心范式转移：从自然语言证明到形式化代码
要理解AI对数学的冲击，首先要明白传统数学证明与形式化证明的根本区别。这不仅仅是媒介从纸笔到屏幕的变化，而是思维范式的深层转换。
2.1 自然语言证明的模糊性与形式化证明的精确性
传统的数学论文使用自然语言（如英语、中文）混合符号来表述。它的优势是富有启发性，便于在人类之间传播思想。但它的致命缺陷是模糊性。自然语言中大量依赖隐含的上下文、默认的共识和“显然”的推理跳跃。例如，“考虑一个足够大的N”这句话，在形式化系统中必须明确：多大才算“足够”？这个“大”依赖于哪些参数？每一步推导所调用的公理或引理必须被显式地指明。
形式化证明则将数学对象（集合、函数、数）和逻辑规则（与、或、非、量词）全部用一套严格定义的符号系统（即形式语言）来表达。一个命题就是一个符合语法的字符串，一个证明就是这个字符串通过一系列预先定义的推理规则（如假言推理）进行变换的序列。Lean、Coq这样的交互式定理证明器，其核心就是一个类型检查器。在它们的世界里，每个数学对象都有其“类型”，每个证明步骤都是一次“类型构造”。如果你声称证明了命题P，那么你必须提供一个类型为P的项（term）。证明器的工作就是检查你构造的这个项的类型是否为P，这个过程是完全机械、无歧义的。
举个例子，我们想证明“自然数的加法满足交换律”。在纸上，我们可能用数学归纳法，写几行推导。在Lean中，它看起来更像一段程序：
theorem add_comm (m n : ℕ) : m + n = n + m := by induction n with | zero => simp | succ n ih => simp [Nat.add_succ, ih]这段代码定义了一个定理add_comm，它接受两个自然数参数m和n，并声称m + n = n + m。证明部分（by之后）使用归纳法。induction n表示对n进行归纳。在归纳基础步（zero），simp策略利用已有的定义简化目标。在归纳步（succ n ih），我们有了归纳假设ih: m + n = n + m，然后利用自然数加法的后继定义Nat.add_succ和归纳假设再次简化，完成证明。Lean内核会逐行检查，确保每一步变换都符合底层逻辑规则。
注意：初次接触时，你会觉得这比手写证明繁琐得多。确实，形式化一个简单的已知结论，其工作量可能远超预期。但它的价值在于可积累性和绝对可靠性。一旦
add_comm被形式化并存入库中，未来任何更复杂的证明都可以像调用函数一样放心地使用它，无需再怀疑其正确性。
2.2 AI大语言模型：从“翻译官”到“猜想生成器”
如果形式化证明的门槛如此之高，那么AI的作用在哪里？早期的定理证明自动化研究主要依赖符号计算和决策过程，对于需要创造性步骤的证明往往无能为力。大语言模型的出现改变了游戏规则。
首先，LLM（如GPT-4、Claude 3、专精数学的Proof-Pile训练模型）可以充当强大的“自然语言到形式化语言”的翻译器。数学家可以将一段用自然语言描述的证明思路或一个猜想输入给AI，AI能够生成大致的Lean或Coq代码框架。这极大地降低了形式化的入门门槛。例如，你可以对AI说：“在Lean中，定义一个拓扑空间，并证明两个紧致子集的并集仍然是紧致的。”AI可以生成大致的定义、定理陈述和证明策略骨架，尽管细节可能需要人工调整。
其次，也是更革命性的，LLM可以作为证明策略（Tactic）的自动生成器。在交互式证明器中，用户通过输入一系列“策略”（如simp、rewrite、apply）来逐步推进证明。这就像下棋，每一步都有很多可能的走法。LLM可以分析当前的“证明状态”（即当前需要证明的目标和已有的假设），预测下一步最可能成功的几个策略，甚至直接生成一整段策略序列。这相当于为数学家配备了一个实时、全知的“提示引擎”，极大地加快了证明的探索速度。
最后，LLM展现了提出新猜想和发现新联系的潜力。通过在海量的数学文献和形式化库上进行训练，AI可以识别出人类尚未注意到的模式，提出可能成立的数学命题。例如，它可能发现两个看似无关的数学结构在形式化描述中具有相似的性质，从而提示研究者去探索它们之间是否存在更深刻的联系。这不再是简单的“辅助计算”，而是开始触及数学发现的源头——提出好问题。
3. 实战：用Lean+AI协作完成一个微型形式化证明项目
理论说得再多，不如亲手试一次。我们以一个具体的、足够小的但非平凡的数学问题为例，展示如何结合Lean和AI辅助（这里以类似ChatGPT的LLM为假设协作工具）来完成形式化。我们的目标是：形式化证明“平方数模4同余于0或1”。这是一个初等数论中的经典结论，证明不难，但涉及定义、量词和案例分析，非常适合作为入门案例。
3.1 环境搭建与项目初始化
首先，你需要安装Lean。目前最推荐的方式是使用VSCode配合Lean4扩展。
- 安装VSCode：从官网下载安装。
- 安装Lean4扩展：在VSCode扩展商店搜索“lean4”并安装。这个扩展会引导你安装Lean工具链和管理项目依赖。
- 创建项目：打开终端，使用Lake（Lean的包管理器）创建一个新项目。
lake init my_number_theory_project cd my_number_theory_project code . # 用VSCode打开项目 - 等待环境就绪：VSCode打开后，Lean扩展会自动下载并构建核心库（
Mathlib）。Mathlib是Lean社区共建的巨型形式化数学库，包含了从基础逻辑到前沿数学的巨量定义和已证明定理。首次打开可能需要较长时间下载。
3.2 定义问题与初步构思
我们的目标定理用自然语言表述是：对于任意整数n，其平方n^2除以4的余数只能是0或1。
在Lean的Mathlib中，整数和模运算都已经有了完善的定义。我们不需要从头定义整数，只需要利用现有的库。打开项目中的MyProject.lean文件（或新建一个SquareMod4.lean），开始编写。
首先，我们引入必要的命名空间和打开常用语法：
import Mathlib.Tactic -- 引入常用证明策略 open Nat -- 打开自然数命名空间，方便使用其中的符号现在，思考如何形式化这个命题。我们需要表达“对于所有整数n，存在一个余数r（r = 0或r = 1），使得n^2 ≡ r [MOD 4]”。在Mathlib中，模同余的表示法是a ≡ b [MOD m]。所以我们的定理可以写成：
theorem square_mod_four (n : ℤ) : n^2 ≡ 0 [ZMOD 4] ∨ n^2 ≡ 1 [ZMOD 4] := by -- 证明体待填充ℤ表示整数类型。[ZMOD 4]表示模4的同余（Z代表整数）。目标是用by块内的策略来构造这个“或”命题的证明。
3.3 借助AI生成证明思路与策略代码
到了关键一步。我们可以将自然语言描述的证明思路喂给AI，让它帮我们生成Lean策略代码。
人类思路：任何整数n模4的余数只能是0, 1, 2, 3中的一个。我们只需对这四种情况分别进行验证（即分类讨论）。计算每种情况下n^2模4的值：
- 若
n ≡ 0 [MOD 4], 则n^2 ≡ 0 [MOD 4]。 - 若
n ≡ 1 [MOD 4], 则n^2 ≡ 1 [MOD 4]。 - 若
n ≡ 2 [MOD 4], 则n^2 ≡ 4 ≡ 0 [MOD 4]。 - 若
n ≡ 3 [MOD 4], 则n^2 ≡ 9 ≡ 1 [MOD 4]。 因此，在所有情况下，n^2模4同余于0或1。
将这段描述和当前的定理陈述一起输入AI（例如：“在Lean4中，我已经定义了定理square_mod_four，需要证明它。证明思路是对n模4的余数进行四种情况的分析。请帮我写出完整的Lean策略证明。”）。
AI可能会生成类似下面的代码：
theorem square_mod_four (n : ℤ) : n^2 ≡ 0 [ZMOD 4] ∨ n^2 ≡ 1 [ZMOD 4] := by have h := Int.emod_add_ediv n 4 -- 将n表示为 4*q + r 的形式，其中r是余数 rcases h with ⟨q, r, hr, hr4⟩ -- 分解出商q和余数r，hr是余数性质，hr4是范围 have r_lt : r < 4 := hr4 have r_nonneg : 0 ≤ r := hr.1 interval_cases r -- 对r在[0,4)区间内进行情况分析，会自动生成r=0,1,2,3四种情况 · -- Case r = 0 left calc n^2 = ((4 : ℤ)*q + 0)^2 := by rw [hr] _ = 16*q^2 := by ring _ ≡ 0 [ZMOD 4] := by dsimp [Int.ModEq] rw [show (16 : ℤ) = 4*4 by ring] exact ⟨4*q^2, by ring⟩ · -- Case r = 1 right calc n^2 = ((4 : ℤ)*q + 1)^2 := by rw [hr] _ = 16*q^2 + 8*q + 1 := by ring _ ≡ 1 [ZMOD 4] := by dsimp [Int.ModEq] rw [show (16 : ℤ) = 4*(4*q^2 + 2*q) by ring] exact ⟨4*q^2 + 2*q, by ring⟩ · -- Case r = 2 left calc n^2 = ((4 : ℤ)*q + 2)^2 := by rw [hr] _ = 16*q^2 + 16*q + 4 := by ring _ ≡ 0 [ZMOD 4] := by dsimp [Int.ModEq] rw [show (16*q^2 + 16*q + 4 : ℤ) = 4*(4*q^2 + 4*q + 1) by ring] exact ⟨4*q^2 + 4*q + 1, by ring⟩ · -- Case r = 3 right calc n^2 = ((4 : ℤ)*q + 3)^2 := by rw [hr] _ = 16*q^2 + 24*q + 9 := by ring _ ≡ 1 [ZMOD 4] := by dsimp [Int.ModEq] rw [show (16*q^2 + 24*q + 9 : ℤ) = 4*(4*q^2 + 6*q + 2) + 1 by ring] exact ⟨4*q^2 + 6*q + 2, by ring⟩3.4 代码解析、调试与优化
AI生成的代码提供了一个很好的起点，但它可能不是最优的，甚至可能有小错误（比如对Mathlib中具体定理名称的误用）。我们需要理解并调试它。
理解关键策略：
Int.emod_add_ediv n 4：这是一个定理，断言任何整数n都可以写成4 * (n / 4) + n % 4的形式。这里用它来获取余数。rcases：用于分解存在性命题或合取命题，将结构体中的字段提取为新的变量。interval_cases r：这是一个非常强大的策略。它知道r是一个满足0 ≤ r < 4的整数，会自动将其拆分为r = 0,r = 1,r = 2,r = 3四个子目标，并分别进行证明。这完美对应了我们的分类讨论思路。calc：构造计算证明块，通过一系列等式或同余式连接，使证明过程清晰。dsimp [Int.ModEq]：简化≡ [ZMOD 4]的定义，将其展开为4 ∣ (a - b)（即4整除a与b的差）。
常见调试与优化：
错误：AI可能使用了错误的前提定理名。例如，
Int.emod_add_ediv在最新Mathlib中可能名称有变。如果报错“未知标识符”，可以将鼠标悬停在错误上，VSCode会提示可能的正确名称，或者使用#print命令搜索，或直接查阅Mathlib文档。优化：上述证明虽然正确，但有些冗长。
Mathlib很可能已经内置了关于平方数模4的结论。我们可以尝试更简洁的证明。实际上，在Mathlib中搜索后，我们可能发现一个更简单的证明：import Mathlib.Data.ZMod.Basic theorem square_mod_four_simple (n : ℤ) : n^2 ≡ 0 [ZMOD 4] ∨ n^2 ≡ 1 [ZMOD 4] := by have := show ∀ z : ZMod 4, z^2 = 0 ∨ z^2 = 1 from by decide simpa [Int.coe_castRingHom] using this n这个证明更高级：它利用了
ZMod 4这个有限环的类型，通过穷举法（by decide）验证了环中每个元素的平方只能是0或1，然后将整数n映射到这个有限环上进行判断。by decide策略会调用决策过程自动验证这个有限域上的全称命题。这体现了形式化数学的另一个威力：利用计算力解决有限情况下的枚举问题。交互式推进：在实际操作中，你不需要一次性写出完整证明。可以逐步推进：写下
theorem后，在by后面回车，Lean会进入“证明模式”，显示当前待证明的目标。你可以手动输入策略，如intro n（引入变量n），然后观察目标变化。AI在这里可以作为“策略建议器”，你可以把当前目标状态复制给AI，问它“下一步用什么策略比较好？”
实操心得：与AI协作的最佳模式不是让它“写完整代码”，而是让它充当“超级自动补全”和“策略提示器”。你自己需要掌握证明的整体逻辑和Lean的基本语法。当卡在某个具体步骤时，向AI描述当前目标和你的意图，让它生成几行可能的策略代码，你再进行选择和调整。这能极大提升学习效率和探索速度。
4. 超越证明：AI如何参与数学发现与知识重构
形式化验证只是AI“重启”数学的一个侧面。更深层的变革在于数学知识的创造、组织和传播方式。
4.1 填补证明“间隙”与发现新引理
在数学研究中，很多“显而易见”的步骤其实包含了许多微小的推理跳跃。在形式化过程中，这些跳跃必须被显式地填补。AI大模型，通过在海量数学文本和形式化证明上训练，变得非常擅长自动生成这些“间隙”的证明。
例如，在一个复杂的拓扑学证明中，你可能需要某个集合是“紧致的”这一事实。你记得这应该由之前的某个引理推出，但具体如何应用那个引理需要一些步骤。你可以向AI（或集成了AI的证明助手如Proofster、Lean Copilot）展示当前的假设和目标，并说：“我需要证明这个子集是紧致的，已知它是闭集且包含在一个紧致集中。”AI可以快速生成应用相关定理（如“紧致空间的闭子集是紧致的”）所需的精确策略代码，甚至帮你处理好所有参数传递和类型转换。
更进一步，AI可以主动建议有用的中间引理。当你在证明中反复使用某种类似的结构或计算模式时，AI可以识别出这种模式，并建议你将其抽象为一个独立的引理（Lemma）。这不仅使当前证明更清晰，也为未来的证明积累了可重用的“零件”。这正是在模拟优秀数学家的思维习惯——识别模式并加以抽象。
4.2 大规模数学知识库的构建与查询
Mathlib这样的项目，其愿景是形式化所有数学知识。这是一个浩如烟海的工程。AI可以加速这一过程：
- 自动形式化经典文献：给定一篇PDF格式的经典数学论文，AI可以尝试理解其内容，并将其中的定义、定理和证明草图转换为形式化代码。当然，这需要人工进行大量的校对和修正，但AI能完成从零到一的草稿工作，将人类从繁琐的编码中解放出来。
- 智能搜索与类比发现：在拥有数十万条形式化定理的
Mathlib中，找到你需要的定理有时如同大海捞针。AI可以构建语义搜索系统。你可以用自然语言描述你的问题（如“一个连续函数在紧集上的一致连续性”），AI能理解其含义，并找到库中相关的形式化定理（如UniformContinuousOn的相关引理）。更强大的是，AI可以基于定理的“形式化签名”（输入输出的类型）和内容，发现不同领域定理之间的相似性，从而提示你可能存在未被发现的数学类比或统一理论。
4.3 教育层面的变革：个性化的“证明教练”
对于数学学习者，AI可以扮演革命性的角色。传统的习题解答往往是静态的、唯一的。而一个集成了形式化验证和AI的数学学习平台，可以提供：
- 无限练习题生成与即时验证：系统可以根据某个知识点（如“归纳法”），自动生成难度递进的、形式化表述的题目。学生尝试用Lean写出证明，系统能立即给出对错反馈。如果证明错误，系统不仅能指出错误所在，还能分析错误类型（是逻辑错误、类型错误还是策略使用不当），并给出针对性的提示，而不是直接展示答案。
- 自适应学习路径：AI可以分析学生在形式化证明中常犯的错误模式，判断其知识薄弱点，然后动态调整后续练习的侧重点。这实现了个性化的“掌握学习”。
- 将“模糊理解”变为“精确理解”：很多学生觉得自己“懂了”一个证明，但让其形式化时却漏洞百出。这个过程强迫学生厘清每一个依赖关系，消除所有“显然”。AI教练在这个过程中不断追问、提示，帮助学生建立起对数学严谨性的深层直觉。
5. 当前局限、挑战与未来展望
尽管前景激动人心，但我们必须清醒认识到当前的局限。
5.1 技术瓶颈：创造力、长程推理与“数学品味”
- 上下文长度限制：复杂的数学证明往往很长，涉及大量前置知识。当前大模型的上下文窗口虽然不断增长，但仍可能无法一次性容纳一个中等规模证明所需的全部背景（定义、引理、中间目标）。这导致AI在辅助长证明时可能出现“遗忘”或连贯性问题。
- 符号推理与计算能力：大语言模型本质上是基于统计的模式匹配器，在需要精确符号计算和深度逻辑推理的步骤上仍然会犯错。它们可能会“幻觉”出一些不存在的定理或错误的推导步骤。因此，AI的产出必须经过交互式证明器的严格校验，这是人机协作的底线。
- 缺乏“数学品味”：伟大的数学发现往往依赖于一种直觉的“品味”，即知道哪些问题是重要的、哪些方向是富有成果的。当前的AI在提出真正深刻、原创的数学猜想方面，还远不能与顶尖数学家相比。它更擅长在人类设定的框架内进行组合和优化。
5.2 实践中的常见问题与排查
在实际使用Lean+AI进行形式化时，你会频繁遇到以下问题：
| 问题现象 | 可能原因 | 排查与解决思路 |
|---|---|---|
| “unknown identifier”（未知标识符） | 1. 定理/定义名称拼写错误。 2. 未导入所需的模块（ import）。3. 未打开正确的命名空间（ open）。 | 1. 使用VSCode的悬停提示或#print命令搜索正确名称。2. 在 Mathlib文档或源代码库中搜索相关概念。3. 检查文件顶部的 import语句是否齐全。 |
| “type mismatch”（类型不匹配） | 这是最常见也最核心的错误。你试图将一个类型为A的项用在需要类型B的地方。 | 1. 仔细阅读错误信息，看它期望什么类型，你提供了什么类型。 2. 使用 #check命令检查相关项的类型。3. 使用 apply?或exact?策略，让Lean帮你搜索可以应用的定理。 |
| 证明状态停滞，不知如何推进 | 对可用的策略不熟悉，或对当前目标的数学含义理解不清。 | 1. 使用obtain、rcases等策略分解假设中的存在量词或析取命题。2. 使用 have语句声明一个中间引理来简化目标。3.将当前整个证明状态复制给AI，询问“我现在有这些假设，要证明这个目标，下一步该用什么策略？” |
| AI生成的代码无法通过验证 | AI“幻觉”了不存在的定理，或使用了过时/错误的语法。 | 1.不要盲目相信AI代码。将其作为草稿，逐行理解。 2. 对AI使用的每个陌生策略或定理名，用 #help或文档查询其含义。3. 将大段AI代码分解，逐步验证。 |
| 编译速度极慢或内存占用高 | Mathlib规模巨大，项目依赖复杂，或证明中使用了低效的策略。 | 1. 确保使用Lake管理项目，并利用其缓存机制。 2. 避免在证明中滥用 simp（简化策略）而不指定范围，这可能导致系统尝试简化所有东西。3. 对于复杂的计算证明，考虑使用 native_decide或norm_num等专门的高效决策策略。 |
5.3 生态与社区：拥抱开源与协作
Lean和Mathlib的成功完全建立在开源社区之上。参与其中，不仅是使用工具，更是参与一场重塑数学知识表达方式的运动。
- 从使用到贡献：当你形式化了一个小结论，并且觉得它可能对他人有用时，可以考虑向
Mathlib提交PR（拉取请求）。贡献流程包括在GitHub上创建分支、编写代码、通过CI测试、并接受社区核心成员的代码审查。这是一个学习最佳实践和深入理解库结构的绝佳机会。 - 学习资源：除了官方文档，关注社区论坛（如Lean Zulip聊天群）、优秀博客和视频教程。许多资深贡献者会分享他们的形式化经验，这些是比官方文档更鲜活的学习材料。
- 找到你的细分领域：
Mathlib覆盖极广，但不同领域的完善程度不同。你可以结合自己的数学兴趣，选择某个方向（如组合数学、代数几何、分析学）进行深耕，成为该领域在形式化方面的专家，填补库中的空白。
这场由AI与形式化验证共同驱动的“重启”，其终点并非取代数学家，而是为我们提供前所未有的思维增强。它将数学家从繁琐的细节验证中解放出来，更专注于高层的概念创造和联系发现；它为数学教育提供了精准的反馈工具；它最终可能为我们留下一个所有细节都经过机器核验的、永不磨灭的数学知识宝库。这个过程充满挑战，但每一步推进，都让我们对“理解”本身，有了更深刻、更精确的把握。
