证明充裕时代：形式化证明如何重塑数学工作计量单位

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体验里核心证明只花了一晚上就过了剩下两天半全部在处理“边界情况”——自然数乘法的交换律、某些变量的空集情况、以及一个特定类型的类型类实例查找失败。每次我修复一个边界情况旧的证明又会冒出一个新的类型错误因为全局上下文变了之前的构造不再合法。这种经历让我一度对形式化工具产生过很重的挫败感。后来和一位做形式化方法有五年经验的同事聊他跟我说了一句让我记到现在的话“把一个证明推进到‘看起来全对’很容易难的是让它‘一直是好的’——尤其是当你的证明库还在不停增长的时候昨天你依赖的那个类型类定义今天可能就被社区改掉了你的整个证明可能就因为这个‘外部依赖更新’而全部失效。”这其实说明了一个很现实的问题为了把数学工作做成一个可重现、可复用的单位你必须付出维护成本。它不是一次性的“写出来就永远有效”而是一个持续需要照顾的活体系统。在当前这个阶段这个维护成本是相当高的。我不建议每一个数学工作者都立刻把自己的所有论文形式化但我强烈建议每一个人都花时间理解这套思维模式——因为它带来的模块化意识、可验证意识、边界条件意识确实能让你传统写作中的证明变得更严谨。说回我个人的体会。我一开始接触“证明充裕性”和“新单位”这些概念时其实是带着怀疑的觉得这又是计算机圈的人跑来“降维打击”数学圈。但真的自己动手拆解过几篇论文、试过用机器逻辑重新复现一段简单证明之后我改变了看法。数学的产出方式确实处在一种变化的过程中我不确定它最终会走向哪里但方向是明确的更细的粒度、更强的验证、更深的复用。对于愿意拥抱这套逻辑的年轻数学工作者来说现在正是最有优势的入场时间——你们既懂传统证明的直觉美又有余力学新工具的手艺两者能碰撞出来的东西比我这种半路出家的人要多得多。最后再分享一个小建议无论你后续会不会真的去做形式化证明从现在开始把自己每一次“显然”的地方都在笔记里补上实际的推理链。这个习惯养成了你会突然发现你手头很多证明比想象中要“年轻”也更有成长空间。