1. 先盘一盘现象：证明真的变“多”了吗
我是从2016年前后开始认真跟踪arXiv上数学板块的更新列表的。当时一天的新文章数量大概在一百篇上下浮动，数学圈的老前辈们已经在抱怨“根本看不完”。到了最近两年，这个数字翻了一倍还不止，热门方向甚至会出现同一问题的预印本在几天内接连挂出、彼此引用的场面。于是就有了这个标题真正想谈的问题：我们是不是进入了一个“证明充裕”的时代？以及，当证明的数量多到一个数学家终其一生也无法通读的时候，我们是不是该重新定义一下“一个数学工作”到底按什么单位来计量。
先别急着下结论，我先把观察到的事实摆出来。
1.1 论文数量的量级变化
用数据说话。arXiv的math板块在2023年全年的新提交量已经逼近十万篇，这还没算数学物理、计算机科学里大量和数学强相关的交叉内容。作为对比，十年前这个数字只有四万左右。什么概念？就是说现在的数学论文产出速度大约是每周两千篇。哪怕你每天不吃不睡只看摘要，一天能过两百篇已经算效率极高了，一周下来你的阅读速度也追不上新文章产生的速度。
更值得注意的是“预印本先于发表”成了默认模式。我认识不少同行，现在投稿到期刊之前，已经默认把完整版本先挂出来让整个领域先睹为快。以前那种憋大招、一篇文章打磨三年再公开的做法，不能说完全消失了，但确实变得更少见了。
这个变化的直接后果是，数学知识的“流通速率”大幅提升。以前大家等审稿要等一年半载，现在预印本一出来，活跃的研究者几天之内就会读到，然后立刻跟进、推广、否定或者改进。一轮又一轮的快速反馈，催生出的新问题和新结论呈指数级膨胀。
1.2 单篇证明的长度与粒度在变化
除了篇数变多，单篇工作的“证明形态”也在变。二十年前的论文，核心定理通常配一个三五页的证明，整个论证链条可以在一页纸里写出一个漂亮的鸟瞰图。但现在很多工作是“大定理+长证明+大量引理”的结构，一个主定理的证明动辄五六十页，中间拆出十几个引理，每个引理又引三个子引理。这类工作单篇的信息量极大，但读起来极其痛苦。
我印象很深的一篇代数几何论文，主定理证明只有开头两行和结尾两行是真正的主线论证，中间四十七页全部是“为证明准备的引理”。这些引理单独拎出来任何一个，在十年前都够写一篇体面的短文。但作者把它们全部压进了一篇论文里，只为了让主定理的证明链条完整闭环。
这就是“证明充裕”时代的第二个特征：证明不再是一个单纯的逻辑推导过程，而变成了一个可拆解、可组合、可复用的工程结构。单个引理就是一块乐高积木，把足够多的积木拼起来，你就能得到一个过去不敢想象的宏大结论。
2. 为什么会有证明的充裕性
你可能会问，这背后是纯数学的自然演进，还是有什么外力在推动？我的判断是，数学内部的发展节奏变化是一方面，但更重要的是一批外部因素彻底改变了数学家组织工作的方式。
2.1 数字化协作让证明变成了可并行任务
先说协作方式的改变。以前一个复杂定理的证明，基本是“一个人闷头干三五年”或者“两三个人咬着牙接力”。一个重要原因是，证明过程中那些零碎的检查、验证、试错，很难在分散的人之间高效交接。你费劲想了三个月的引理，可能只是人家整体框架里一个需要被确认的细节，但你们之间沟通的成本高到让人不想碰。
现在不一样了。Overleaf让所有人实时编辑同一份LaTeX文档，Git仓库可以记录每一次改动，一个主定理的证明可以被拆成十几个独立小节，分给不同的人。每个人只需要确保自己负责的小节逻辑自洽，然后通过一个公开文档把各部分的接口定义清楚就行。这种工作模式，本质上把证明变成了一个可并行的任务。并行带来的是什么？是单纯的效率提升吗？不，并行带来的是产出量的暴涨——原来一个团队一年只能完成一个核心定理的完整证明，现在同样的团队可以在同一时间段内完成三个或者四个，因为大量的中间步骤是同步推进的。
2.2 预印本文化把“未完成品”也放进了流通池
以前数学论文有一个心照不宣的规矩：公开的东西必须“完整”。这个完整不仅指逻辑完备，还包括审美上的圆满——你的证明应该给人一种“这件事做完了”的感觉。很多数学家宁可把结果压在抽屉里，也不愿意拿出一个“虽然对但不好看”的版本。
预印本文化的兴起把这道门槛拆掉了。现在大家可以放心地把一个还没完全打磨好的结果挂出来，哪怕第五十七页那个引理还带星号标注“该引理证明稍后补充”，读者也不会觉得这是学术不端，大家已经默认这会后面更新版本。这种“先释放，再完善”的模式，极大降低了公开一项数学工作的心理成本和时间成本，也让大量原本会烂在学者电脑里的半成品、可改进品、甚至失败品的部分有效片段全部流入了公共领域。
我见过一个例子，有人把一个证明框架挂到预印本上，主定理的证明只完成了一半，但框架写得极其漂亮。三个月后，另外两组人各自补齐了剩下那一半，用的还是完全不同的思路。一篇半成品，催生了两条完整的新路线。这在以前是不可想象的。
2.3 计算机辅助证明改变了“完成”的定义
第三个因素，我个人认为是真正意义上的“单位转变”：计算机辅助证明，尤其是交互式定理证明器（Interactive Theorem Prover），把“证明完成”这件事从一个模糊的精神状态变成了一个可机械验证的客观事实。
以前你说“这个证明完成了”，意思是“我自己反复检查了十遍，给两个同行看过，他们也没发现问题”。但可验证性完全取决于参与者的水平、细心程度和运气。1990年代那场关于拓扑学里某个著名问题的争论，就是两篇论文互相指责对方证明里的一个关键步骤有误，谁都无法说服谁，最后这句话悬了十几年才被人用计算机辅助验证彻底解决。
而在Lean或者Coq这类系统里，“证明完成”只有一个含义：机器在类型系统层面认可了你构造的这个证明项，所有推理规则都通过了检查，没有第三步，没有可争议的灰色空间。这个转变意味着，一个数学工作的“完成”不再依赖某个权威人类读者，而是依赖一个完全公开、可复现的验证过程。当所有同行都可以下载你的代码库，一个人花五分钟把自己的名字加进Lean的编译系统，逐字逐句跑一遍你的证明管线，这个工作就被确认了。
这就是我所说的“新单位”。一个数学工作，正在越来越像一个可以被编译、被验证、被重构的工程模块，而不是一段仅供人类智力欣赏的思维瀑布。
3. 新单位：形式化证明如何重塑工作计量
我猜很多读者看到这里会觉得，这又是那些鼓吹AI替代数学家的人在那瞎操心。我明确说，我不认为机器在短期内能取代数学家做真正的创造性思考，但形式化证明带来的“计量单位”变化，是实实在在正在发生的，而且影响面远比你想象的大。
3.1 从“思想”到“可执行对象”
先解释一下交互式定理证明器做了什么。以Lean为例，它的核心是一个类型论逻辑系统。你在Lean里写的每一个定理、每一条引理，本质上都是一个“类型”——而证明这个定理，就是构造出这个类型的某个“实例”。
我用一个不太精准但足够直觉的类比：把Lean想象成一个超级严格的解题老师，你的任务是向它证明某个命题是真的，你可以用任意技巧——分解、转换、引用之前证明过的定理、用归纳法——但每一步都必须经过它预先设定好的推理规则库的检查。它不关心你的证明是否优雅、是否漂亮、是否符合数学家的品味，它只关心：从已知的真命题出发，你的每一步推导是不是严格符合逻辑规则。如果是，证明通过；如果不是，它会准确地告诉你“这里有一个类型错误”或“这条路径没有通过检查”。
一旦证明通过检查，它就不再依赖任何主观判断了。任何人在任何时间重新编译这段代码，都会得到同样的结果。这个特性在推动着一件非常重要的事：把证明从“思想产品”转向“可执行对象”。
当一个证明变成可执行对象之后，计量它大小的单位也变了。你不能再用“页数”或者“字数”来统计一个证明的工作量，因为这些指标完全取决于作者的个人风格。有的数学家喜欢把一个引理写成三十行，有的喜欢用三段话加一个注记搞定。但Lean里面的证明长度单位是“符号数”“战术调用次数”“依赖定理的数量”，这些都是固定的、可统计的、无歧义的。
我见过有人统计过，一篇传统的二十页论文，如果把它完整形式化到Lean里面，证明代码通常会长达五千到一万行。而一个只有三行核心证明的著名定理，形式化之后往往要一百多行代码来处理各种边界条件。这就产生了一个非常反直觉的衡量结果：代码行数，而不是页数，成为了一个更接近真实工作量的指标。
3.2 新单位的粒度：定理是一等公民
在传统数学写作里，证明确实存在于论文里，但它的“存在方式”是叙事性的。读者需要理解作者在做什么、为什么这样做、接下来的步骤为什么自然。这在传递深层直觉时是必要的，但也带来了一个副作用：证明和证明之间的依赖关系是隐含的，A用到了B的第几个引理，你不把全文读明白，根本看不出来。
形式化证明不一样。在Lean的数学库里，每一个定理都拥有独立的命名空间、独立的依赖列表、独立的类型签名。你调用一条引理的时候，系统会精确地告诉你它依赖哪些更基础的定理，这些依赖又能一路追溯到自然数公理。这意味着整个数学知识体系变成了一棵严格的、可查询的、无环的依赖树。定理在这个体系里不是散落的金句，而是一个个有明确身份和边界的“公民”。
这样的数学工作计量单位就从“论文”变成了“定理”，从“一本著作”变成了“一个数学库”。你不再说你今年写了两篇论文，而是说你向Mathlib贡献了一百八十个新引理，修复了六个旧引理的类型定义错误，把某个关键定理的证明长度从两千行压到了一千二百行。这些在传统数学世界里根本不存在的工作内容，正在成为新的数字劳动。
3.3 对数学家时间分配的影响
我不想把形式化证明吹成救世主，因为它确实还有巨大的学习成本和不成比例的投入。但有一件事是确定的：它已经在深刻改变一部分数学家分配时间的方式。
在我和一些研究者的交流里，明显感觉到两种态度的撕裂。老派数学家普遍觉得，花两个月把一个两页纸的定理形式化，是纯浪费时间，因为这时间本可以用来做三倍的新思考。而年轻一代，尤其是博士阶段就开始接触Lean的学者，往往会主动把自己的新证明同步形式化，哪怕这个过程让一篇文章的完成时间翻倍。
年轻一代的逻辑其实很简单也很现实：一个形式化过的定理，它的可复用性比一个只存在于PDF里的定理高出一个数量级。你的证明被Mathlib收录之后，全世界几百个正在用Lean做研究的团队，在遇到和你的定理相关的步骤时，会直接调用你的工作，而不会有任何磨损，也不会产生任何沟通成本。
我见过一个做代数数论的年轻同行，他的博士论文核心定理在完成传统证明后的两个月内，就被他完整地形式化进了Lean。当时我还笑他自找苦吃，结果半年后，另一个做算术几何的研究组在构建一个大证明时，在一百多个步骤里用到了他那个定理四次。他的工作成了那个更大证明中不可替代的基石。这种“一次完成，到处使用”的复用模式，正是“新单位”最有力的体现。
4. 一个外行也能上手的参考路径（实操向）
说了这么多抽象层面的东西，肯定有读者想问：那这东西跟我有什么关系？我又不是做数理逻辑的。我要说的是，就算你不做形式化证明，理解“证明作为一种工程对象”的思维方式，对你做任何需要严谨论证的事情都有帮助。这一节我会给出一个我亲测有效的参考路径，帮你零基础体会到“新单位”到底是怎么运转的。
4.1 第一步：先别急着学Lean，先学会“拆证明”
很多人一听到形式化证明，第一反应就是去装Lean、配环境、写代码。我的建议恰恰相反：先老老实实拿你手头一篇熟悉的数学论文，做一次“拆解练习”。
选一篇你自己方向里的经典论文，不要选太长的，最好是一篇十页以内、主定理只有一个、证明不超过五页的。然后拿出一张白纸，不要看文章里的原有结构，自己从头开始重新把它拆成这样的清单：
- 主定理依赖哪些核心引理？
- 每个引理自身又依赖哪些子引理？
- 哪些步骤用到了文中之前的结果？
- 哪些步骤用到了约定俗成但没有明说的背景知识？
- 哪些步骤是那种“显然”但仔细验证其实很费劲的？
这看起来很简单，但做一遍你就知道，真实的数学论文里充满了“显然”和“由前文可知”，这些词背后往往藏着大量的隐含前提。我在拆第一篇论文的时候，发现作者在证明中段用了一个“由标准结果可知”的命题，翻遍全文也没找到这个标准结果的出处，最后另找了一本专著才发现这是三章之后才出现的定理。这就是传统数学写作的现状：作者对读者的知识水平做了一种理想化的假设，而这个假设在现实中经常不成立。
拆解完之后，用红色笔在每一条引理前面标上“模块名”，比如“引理A：模p约化保持稳定化子”“引理B：某曲面上不存在奇异向量”这样的命名格式。这一步做完，你会发现原本一个模糊的大证明，其实是由十几个边界清晰的积木块拼起来的。这个“模块化直觉”，比任何工具都重要，它是你理解后面所有内容的基础。
4.2 第二步：把证明当工程——模块化、再验证、回归测试
有了拆解练习的基础，你可以试着用工程思维重建这个证明。什么叫工程思维？就是多问几个“如果……怎么办”：
- 如果把引理A的证明替换成另一种方法，后面的主线证明会不会被破坏？
- 如果把引理B的假设条件削弱一点，结果还成立吗？如果成立，后面的证明是否可以变得更一般？
- 有没有可能调整模块顺序，让整个证明的主干更短、依赖更浅？
这些问题是传统数学写作里不太有人问的，因为论文是线性的叙事，你一般都顺着作者的思路走。但当你把证明当作工程对象来看待时，你会发现它们的结构不是唯一的。我见过某位同行把一篇论文里的六个引理重新编排之后，整个证明长度缩短了将近三分之一，衍生出来的新工作也比原文多出了一倍不止。
做完重新编排之后，就是“回归测试”，这是我特别想强调的一步。当你对证明的某个模块做了修改，即使是很小的修改，你也必须重新走一遍主线论证，确保修改后的模块和所有依赖它的部分仍然是兼容的。如果不兼容，问题出在哪？是模块的接口定义变了，还是主线论证里对旧接口的调用没有被同步更新？
这种“回归测试”的自觉，在传统数学训练里几乎不存在。大家默认“改一下证明里的某个引理，其余部分重新读一遍没问题”，但实际上，人的注意力很容易被你改动过的地方吸引，而真正的隐患往往藏在那些你认为完全没变的地方。我有一次修改了一篇论文里的一个定理证明，只改动了一个条件从“处处非零”到“局部非零”，当时我确保主线每一步都没问题，结果投稿后审稿人发现，我在论文后面一个不起眼的推论里，调用了这个定理的时候，默认它还保留着“处处非零”的旧条件。
这就是为什么我现在会在自己每一篇论文的最终清稿阶段，都会强制自己做一个“依赖检查清单”——把每个定理和引理，它们分别用了哪些前置结果，用完整列表写出来，逐个勾选。这本质上就是把Lean里面那种自动依赖跟踪，用最笨的手工方式做了一遍。你不需要任何高层次工具，就能体验到“新单位”带来的直接好处——它逼你对你自己的数学工作负上比传统写作严格得多的责任。
4.3 第三步：一个极简可验证的小练习
如果你想真正碰一下“机器检查证明”这个过程到底是什么感觉，我推荐你不用直接上Lean或者Coq这种重型系统，而是找一个更轻量的入口：布尔逻辑解题小工具或者SAT求解器。
拿SAT来说，它的核心问题是解决“给定一堆布尔变量和它们之间的约束条件，是否存在一组赋值让所有约束同时成立”。看起来和数学证明八竿子打不着，但我给你一个具体的练习标准，你就知道为什么它适合上手：
- 取一个你熟悉的数学命题，要求它只涉及赋值和逻辑关系，比如“对任意整数x，如果x是偶数，那么x的平方是偶数”。
- 把这个命题尽可能拆成小的布尔变量定义和约束。
- 用SAT求解器检查这个约束系统是不是可满足。如果可满足，说明存在满足所有条件的对象。如果不可满足，说明你的命题内部存在逻辑矛盾。
- 然后尝试给这个约束系统加入一条新约束，比如“x同时是奇数”，再看求解器的判断会怎么变。
这个练习看起来简单，但做完你会得到一个切身体会：一个证明，或者任何一个逻辑论证，在机器眼里只是一个约束满足问题。你的所有已知条件都是约束，你的结论是不是必然成立，取决于在所有约束都满足的情况下，结论是不是必然为真。
我至今记得自己第一次用SAT求解器验证一个“显然”的数学命题时的震撼。那个命题在纸上写出来，任何人都会觉得“这不需要证”，但当我试图把它转成约束系统时，发现我漏掉了一个边界条件。这个边界条件在传统数学写作里根本不会被注意到，但在机器检查的框架里无处遁形。从那一刻起，我才真正理解了为什么很多人说形式化验证提升的是你的严谨性，而不是你的数学直觉。
5. 一堆真实踩坑记录与常见误区
最后这部分，我想把这几年来在实际尝试、以及在和不同做形式化证明的同行交流过程中积累的踩坑记录做一个集中整理。很多新手，包括当初的我自己，都是因为对这件事有一些过于乐观或者过于悲观的误解，导致在实践过程中走了不少弯路。
5.1 误区：形式化证明＝查bug工具
第一类常见误解，是把形式化证明当成“检查你传统证明有没有错的工具”。这个想法完全可以理解——毕竟Lean确实能发现你证明里被遗漏的步骤。但我要告诉你，把形式化当作查bug工具，会让你极其痛苦。
原因是：传统证明里的大多数步骤是可以被人类智力自动填充的，而形式化系统不会自动填充任何东西。你写“显然A蕴含B”，在Lean里这需要你真地构造一个从A到B的函数或者逻辑转换，哪怕这中间只是使用了一条蕴涵引入规则。也就是说，形式化一个证明，大多数时候不是“检查”你的旧证明，而是“重新写一遍”這個证明，只不过这次语言变成了机器的类型论语言，而不再是人类的高效简写。
我最初尝试形式化一个三页纸的引理时，预计花两天，最后整整耗了两周。不是因为原证明有错——它没有错——而是因为原证明里的每一个“显然”和“不难发现”，我都需要找到精确的Lean战术组合来实现。这种感觉就像你把一篇文章从口语翻译成文言文，信息量完全一样，但努力程度不在一个量级。
5.2 误区：证明充裕＝质量稀释
再说第二个误区，也是我在社交平台上看得最多的抱怨：“论文越来越多了，但水分也大了。”我不认识任何。这种担心的确有一定道理——任何数量的指数增长，都会带来一定比例的良莠不齐。
但“证明的充裕性”和“质量下降”之间不构成因果。论文之所以变多，不是因为大家开始注水，而是因为三个我在前面仔细解释过的结构性原因：并行协作降低了完成大证明的时间成本，预印本文化拉低了公开作品的门槛，以及形式化工具让证明可以被机械验证而不再依赖权威背书。这三个原因，每一个都是在提升数学工作的效率和质量可控性，而不是在稀释它们。
你看到的“那篇论文好像没什么有用的东西”，很可能只是因为它的目标读者不是你，或者它是在一次协作中某个确定模块的中间产出——单独看它，确实不够“惊人”，但它是那个更大的、惊人的数学结构的一部分。用我前面说的“单位思维”来看，如果你还以“一篇论文”为基本单位来衡量所有工作，你自然觉得质量不行。但如果你把“一个模块化的引理”看作基本单位，你会发现它的价值和完成度其实是很高的。
5.3 实操坑：形式化验证的“最后一公里”最难
如果说前两个误区还只是认知层面的，下面这个坑则是纯粹的操作层面，而且几乎所有人都会遇到。那就是：你花了百分之九十的时间把证明从开头推进到临门一脚，剩下百分之十的“琐碎收尾”却要用掉你另外百分之九十的时间。
我在一次Lean体验里，核心证明只花了一晚上就过了，剩下两天半全部在处理“边界情况”——自然数乘法的交换律、某些变量的空集情况、以及一个特定类型的类型类实例查找失败。每次我修复一个边界情况，旧的证明又会冒出一个新的类型错误，因为全局上下文变了，之前的构造不再合法。
这种经历让我一度对形式化工具产生过很重的挫败感。后来和一位做形式化方法有五年经验的同事聊，他跟我说了一句让我记到现在的话：“把一个证明推进到‘看起来全对’很容易，难的是让它‘一直是好的’——尤其是当你的证明库还在不停增长的时候，昨天你依赖的那个类型类定义，今天可能就被社区改掉了，你的整个证明可能就因为这个‘外部依赖更新’而全部失效。”
这其实说明了一个很现实的问题：为了把数学工作做成一个可重现、可复用的单位，你必须付出维护成本。它不是一次性的“写出来就永远有效”，而是一个持续需要照顾的活体系统。在当前这个阶段，这个维护成本是相当高的。我不建议每一个数学工作者都立刻把自己的所有论文形式化，但我强烈建议每一个人都花时间理解这套思维模式——因为它带来的模块化意识、可验证意识、边界条件意识，确实能让你传统写作中的证明变得更严谨。
说回我个人的体会。我一开始接触“证明充裕性”和“新单位”这些概念时，其实是带着怀疑的，觉得这又是计算机圈的人跑来“降维打击”数学圈。但真的自己动手拆解过几篇论文、试过用机器逻辑重新复现一段简单证明之后，我改变了看法。数学的产出方式确实处在一种变化的过程中，我不确定它最终会走向哪里，但方向是明确的：更细的粒度、更强的验证、更深的复用。对于愿意拥抱这套逻辑的年轻数学工作者来说，现在正是最有优势的入场时间——你们既懂传统证明的直觉美，又有余力学新工具的手艺，两者能碰撞出来的东西，比我这种半路出家的人要多得多。
最后再分享一个小建议：无论你后续会不会真的去做形式化证明，从现在开始，把自己每一次“显然”的地方，都在笔记里补上实际的推理链。这个习惯养成了，你会突然发现你手头很多证明比想象中要“年轻”，也更有成长空间。
