最近在整理自己这几年做数学研究的笔记时有一个感觉越来越强烈我们手里的“证明密度”和十年前完全不是一回事。同事之间互相发预印本动不动就是几十上百页的证明附录里还挂着一堆运行日志和验证脚本。过去我们说“这篇论文贡献了一个定理”现在更常见的说法变成了“我完成了一项可验证的证明工作”。这背后其实是一个值得认真对待的方法论变化——证明越来越丰富数学工作的计量单位正在被重新定义。这篇东西就是想把我对“证明丰裕”现象的理解、一些实操经验、以及我自己踩过的坑整理出来给正在适应这种新节奏的研究生和同行们做个参照。我平时的主要方向是代数和数论近几年也在尝试把部分工作迁移到形式化验证的环境里所以对“证明数量膨胀”和“工作单位变化”这两件事都有切身体会。文章里不会堆太多纯理论的东西更多是讲我实际是怎么处理长证明、怎么拆解验证任务、怎么用现代工具管理自己的数学工作流以及在这个过程中发现的那些容易让人抓狂的细节。1. 证明丰裕是怎么出现的1.1 论文数量与证明长度的双重增长先看一个很直观的指标arXiv上数学类目的月新增量十年前和现在差了好几倍。很多领域的热门方向一个分支方向的论文列表翻一页就要花不少时间。论文多了单篇论文包含的证明也越来越复杂。我不觉得这是因为现在的数学家比前辈更“勤奋”或更“聪明”而是整个学术生产的模式变了。以前一个定理的证明如果超过五十页大家会默认它属于极少数大师才能驾驭的工作现在五十页往上走的证明在代数几何、表示论、解析数论这些方向里已经不算罕见。加上各种引理、命题、推论相互引用一篇论文实际包含的逻辑链条可能比正文看起来还要长得多。体量膨胀的直接后果是传统的“定理—证明”这个叙事单元已经不太够用了。以前同事间交流问一句“你证明了什么”大家默认答案是某个干净漂亮的命题现在更实际的问法是“这个证明你们用机器检查过了吗”或者“关键步骤的脚本还在不在”。这不是说传统的数学品味没有了而是证明本身变成了一种可以拆解、可以批量处理、可以自动化验证的对象它的“可操作性”已经成了衡量数学工作质量的重要标准。1.2 从单打独斗到公开协作另一个推动证明数量增长的因素是协作模式的变化。以前一个大的证明计划核心参与者可能就是一个或两三个人的小团队其他人只能等结果出来之后再慢慢消化。现在不同了公开的协作平台和预印本文化让许多证明项目在早期就能吸引大量参与者每个人的工作都可以细分成很小的单元然后合并进一个大系统里。最典型的例子就是形式化数学社区里那些大型库比如Lean的mathlib。几千个贡献者数万个定理每个定理的证明都被拆成一条条代码提交记录。你贡献一个引理他补一个不等式我再修一个bug整个体系就像大公司里的并行开发流程。这种模式带来了一个很有意思的结果数学证明的“最小工作单元”从“一篇论文里的一个定理”变成了“一条可以被审阅、被编译、被复用的证明记录”。当然不是所有数学分支都适合这种公开协作代数、数论这种偏“手工”的方向真正参与大型协作项目的人还是少数。但即使在小圈子内部大家也有了这样的意识证明不再是一次性的智力表演而是可以长期保存、持续维护、供别人下一步工作调用的“基础设施”。这种意识本身就是证明丰裕的一部分。1.3 机器验证如何改变“证明”的定义我在前年做了一个很小的决定把一个引理的证明搬进Lean里纯粹是想看看现在的形式化工具到底能省多少事。结果那个本来只要两页纸的引理我用了一个下午才搞定中间还反复查库和调试。但搞完之后我突然意识到这个引理在我心里的地位变了——它不再是一个“我觉得是对的”的断言而是一个“无论如何都没法错了”的成品。机器验证对数学工作的冲击就在这里。它没有改变证明的逻辑本质但它改变了证明的社会属性。传统意义上的证明哪怕写得再详细最终还是要靠同行去“相信”形式化验证的证明是靠机器一句一句硬核检查出来的审阅人可以转而关注这个证明的框架是否合理而不是在几百页的符号推导里找漏洞。这种转变的直接后果是数学工作的“单位”从“我证明了什么”向“我验证了什么”倾斜。一篇论文可以放心地引用一个形式化证明过的引理而不必再担心潜在的错误一个大型项目的推进方式也可以改成“先把所有底层引理都验证掉再往上搭结构”。这些变化都在悄悄塑造新一代数学工作者的习惯和产出方式。所以在进入具体操作之前我想先把这个大背景聊透证明越来越丰富验证越来越自动化我们用来衡量“一个数学工作”的单位也在被重新校准。接下来的内容就是我基于这个判断总结出来的一些方法论和实操经验。2. 新的单位从“定理”到“可验证的对象”2.1 传统单位到底哪里不够用以前的数学工作单位往大了说是一篇论文往小了说是一个定理。这两个单位在很长一段时间里都够用因为一篇论文的读者群体会自己想办法消化证明审稿人也会逐段检查关键推理。可当证明的体量上来之后这两个单位就暴露了问题。论文是一个很粗的粒度它没法表达“这个论文里哪些部分是真正的新工作哪些只是搬运”。定理又是一个很短的粒度它没法表达“为了证明这个定理我们余额外构造了几个辅助对象、写了多长的程序、做了多少次计算模拟”。也就是说传统单位在“度量”这件事上做得并不好它只能告诉我们“这里有一个结果”却难以说明“为了得到这个结果需要投入多少可复现的智力劳动”。这就是“新的单位”出现的背景。所谓的“新单位”并不一定是一个精确定义的数学概念而更像是一种共识现在的数学工作至少要能拆成可以被单独验证、单独引用、单独复用的对象。对我个人来说这个单位的直观体现就是“一条验证过的引理记录”它有清晰的输入输出有可编译的代码有可供他人检查的日志整个状态在系统里是透明可回溯的。2.2 可复现性成为数学工作的硬指标传统数学论文里最常见的附录是“手算细节”和“长公式推导”——这些东西当然有价值但最大的问题是难以真正复现。审稿人不会用几周时间把每个公式的推导都重来一遍作者本人也未必能在一年后毫无困难地再现当时的推演过程。可验证的对象不一样。哪怕你的工作是一个很长的程序只要环境和依赖被记录下来别人就可以一键复现整个验证过程这种“可复现性”是传统的手写证明很难提供的。它不是要求每一个数学结果都必须跑代码而是在告诉整个圈子如果你能提供可复现的验证流程你的工作会被更高程度地信任也会更容易被下一代成果引用。我之前参与过一个小型合作项目对方发来的初稿里包含一个关键引理他写的是“这个论断可以直接由标准方法得出”。我们几个人来回看了三遍总觉得中间跨了一步。最后我实在受不了把这个引理做成了Lean里的一个lemma然后才发现需要补三个额外的假设才能让它成立。这个过程本身不复杂但它说明了一件事把证明变成可验证对象的过程同时也是把模糊陈述变成精确数学陈述的过程这种精确化本身就是一种增量工作。2.3 形式化证明、仓库提交记录与协作单元在实际操作层面我体会最深的是新单位往往以“仓库里的提交记录”为物理载体。随便打开mathlib的pull request列表你会看到大量这样的记录有人修了一个转置矩阵的引理有人补了一个积分的边界情况有人把某个集合的有限性判断从“可解”改成“默认成立”。每一项单独看好像都只是小修小补但合在一起就是一个庞大的、不断生长的证明库。这种“颗粒度极细”的工作单元放到传统的学术评价体系里几乎没法识别——你不能说“我修了mathlib里的一个parameter”就当成一篇论文但它确实是现代数学工作不可或缺的一部分而且可以说是基础。一个新定理的形式化证明往往要依赖前面几十个这样细小的提交记录这就是“证明丰裕”的微观面貌。所以我对这个“新单位”的理解可以用一句话概括它不是一个孤立的定理而是“证据链完整、可被集体复验、能在下一步工作中被直接调用”的一个证明对象。它不一定是形式化的但它一定具备可操作和可复现的特质。有了这个单位我们做研究的时候就可以换一种问法不是“这个结果能不能发”而是“这个证明能不能被高效地检查、能不能被其他人快速复用”。这个转变看着小但实际上牵涉到后面所有的日程安排、工具选型和工作习惯。3. 日常研究怎么适应这种变化3.1 把证明当作“工程项目”来管理现在我做比较复杂的证明不会再抱着“我在写一篇优美论文”的心态更像是在做一个工程项目先画模块图看哪些结论是地基哪些结论是承重墙哪些结论只是装饰然后按依赖关系排序从地基开始一点一点搭。这个习惯最初是被逼出来的。有一次我自己写一个三十页左右的证明写到第十五页的时候发现第十页引用的一个结论其实需要更严苛的条件结果导致后面一半内容全部要返工。从那次之后我开始认真记录每一小步的前提条件还会用版本管理工具跟踪这个证明的演进。后来接触Lean之后更发现这种工程化的思路跟形式化验证天然契合——Lean里每个theorem都有明确的声明和上下文依赖关系一目了然改一处定义会立刻影响所有相关的证明。工程化的另一个优势是方便分工。如果一个证明能被拆成若干个相对独立的组件你就能邀请合作者分别负责不同部分每个人只需要保证自己那一块能通过验证就行。这在传统写作方式里很难做到因为大家写在同一篇文章里互相之间的潜在矛盾要到最后排稿时才会爆发在模块化的验证框架里这种矛盾会被系统提前暴露出来避免到最后一刻才手忙脚乱。3.2 选择适合自己的形式化程度不是所有工作都值得100%形式化。我自己有一个比较实用的分层标准在这里分享给大家参考第一层完全形式化。适用于基础性、复用性强的引理以及那些特别繁琐、人肉检查容易出错的推导。这类工作投入大但收益也大因为你以后可以放心地在别的证明里反复引用它们。第二层半形式化。记录清楚每一步的依赖关系、关键计算和边界情况但在叙述方式上仍然保持传统数学论文的样式。这种做法适合大多数中等复杂度的证明既能保证可复现性又不至于被工具折腾到怀疑人生。第三层非形式化但规范化。主要用于探索阶段的草稿不需要生成验证脚本但必须遵守一套自己定的规范比如每个新引入的记号都要写清楚定义域每个估计都要附带误差项每个“显然”都必须标注实际用到哪一个引理。这套分层不一定适合所有人但核心思路是通用的根据你的工作目标和下游使用者的需求决定你要做到多严格的验证。有些基础定理以后别人会大量引用白费功夫去形式化也不亏有些临时性的中间结论你自己知道能用就行非要逼着它走完所有检查流程反而是浪费时间。3.3 工作量评估的私人方法既然数学工作的单位在变工作量评估也应该跟着变。过去我们习惯用“我写了多少页论文”或者“我证明了几个定理”来评估一个阶段的工作但这两项指标在新环境下都不太可靠。论文可能注水定理可能有主次之分单纯计数很容易失真。我自己现在更习惯用“验证单元”的数量和质量来衡量工作量。一个验证单元可以是一条可编译的引理一个跑通过的数值实验一个完整记录的推导流程或者一份能重复出一个图表核心数据的脚本。每完成一个验证单元我就在项目管理表里打一个勾同时记录它依赖了哪些更基础的单元。这样做最大的好处是心里有数哪怕某天论文一个字都没写但只要验证单元列表在稳步变长我就知道工作没有白费只是产出形式暂时还没转化成传统论文而已。反过来如果一周下来一个验证单元都没完成那说明目标设定得不合理或者卡在了某个阻塞点上需要及时调整策略。我还会在月底统计一次各类验证单元的累计情况哪些类型的证明产出效率最高、哪些地方投入产出比太低下个月就开始有意识地调整。这种方法听起来有点“制造业”但确实能帮我在面对大量信息时保持节奏感。4. 用Lean做一个最小可复现示例4.1 环境准备与项目初始化聊了这么多方法论接下来给大家看一个具体的实操例子我用Lean 4来演示怎么把一个简单的数学证明变成可验证的单元。选择Lean而不是其他工具主要因为它的数学库mathlib非常完善代数、分析、拓扑的覆盖面都很广适合做日常验证工作。安装Lean 4的方式不复杂macOS或Linux系统一般用elan来管理工具链。装好之后创建一个项目目录在目录里放一个lean-toolchain文件指定要用的Lean版本然后打开一个.lean文件就可以开始写了。我个人的建议是第一次接触形式化证明的人不要把目标定得太高。不要一上来就想证明一个大定理先写几个非常小的引理跑通整个流程比如自然数的加法结合律、偶数的基本性质之类的等你熟悉了基本的策略语法再逐渐加大难度。4.2 定义偶数和基本证明这里我给一个最小可运行的示例证明“两个偶数的和仍然是偶数”。先定义偶数这个命题再证明闭包性质import Mathlib.Data.Nat.Parity import Mathlib.Tactic.Ring def IsEven (n : Nat) : Prop : ∃ k : Nat, n k k theorem even_add_even {a b : Nat} (ha : IsEven a) (hb : IsEven b) : IsEven (a b) : by rcases ha with ⟨ka, hka⟩ rcases hb with ⟨kb, hkb⟩ rw [hka, hkb] use ka kb ring这段代码的意思很直白我先把两个偶数的定义展开得到它们都是某个自然数加自身的分解然后把这两个分解代入求和的式子接着构造一个新的存在量词令它为kakb最后用ring这个策略证明(kaka)(kbkb)等于(kakb)(kakb)这种形式的恒等式也就是加法结合律和交换律的组合结果。这里有一个值得注意的地方在定义里我故意没采用Nat.Even这样的库函数而是自己写了一个IsEven目的就是展示“从零定义概念再证明性质”的完整流程。实际工作里如果你要用到奇偶性直接用mathlib里现成的定义会更省事但通过自建定义你能更清楚地看到形式化系统是如何把数学概念和逻辑证明绑定的。4.3 实际运行与常见报错处理写完上面的代码后用Lean的编辑器插件比如VS Code的lean4扩展保存一下系统会自动编译并把结果反馈到界面上。如果所有策略都通过代码旁边会没有任何红色波浪线如果有错误也会精确提示是哪一行哪一步出了问题。我第一次跑类似示例时遇到的错误非常典型写use ka kb之后忘了写ring结果Lean告诉我目标没有被完全解决因为存在量词虽然构造出来了但里面还残留着明显的等式变换没有处理。另一个常见问题是rw这个策略只能处理“定义上的相等”如果这是纯粹的代数恒等式直接rw往往不够保险起见还是直接上ring或omega这类更自动化的策略。还有一个容易踩的坑是导入库的问题。Mathlib.Data.Nat.Parity这个名字在不同版本里可能略有差异如果你用的mathlib版本比较新部分文件名可能会有调整。遇到类似情况最简单的办法是搜索mathlib仓库里的对应文件名或者直接改成导入整个Mathlib虽然编译时间会变长但一般不会出现缺失定义的问题。每次成功编译一个theorem我都习惯顺手在边上记一行注释说明这个证明依赖了哪些已知引理或策略方便自己以后复查。这是一种很笨但很有效的方法等你做了几十个引理之后回头查问题会轻松很多。5. 从“人肉证明”到“机械验证”的几个真实坑5.1 形式化不等于没有数学困难我必须强调一点形式化验证并不能代替数学思考。我在Lean里做的很多证明真正的难点不是“怎么把这些命令敲到编辑器里”而是“在没有做形式化之前我对这个命题的理解是否足够清晰”。当你尝试把直觉上的证明步骤翻译成机器能看懂的语言时它往往会逼你重新审视每一个隐式假设然后你才发现原来自己的原证明里藏着一个小漏洞。有一次我在验证一个关于有限群子群数量的引理时原证明里写“由拉格朗日定理这个子群的阶数整除群阶”听起来没什么问题但在Lean里写的时候你必须要明确“这个子群是否可解”“作用在什么集合上”等一堆上下文。补上下文的过程让我发现这个引理其实只在一类特殊情况下成立原证明需要额外加一个前提条件。这种事几乎每天都在发生它恰恰说明了“新单位”的价值验证一件东西等于重新审视它。所以提醒大家不要觉得形式化是“低智力活动”。实际上它和传统数学研究一样需要创造力只不过创造力的方向从“构建一个新概念”转向了“把旧概念建模成精确机器语言”而我个人觉得长期做下来后一种能力的成长对整体数学修养非常有用因为你再也不会说出“这显然成立”这种其实并不显然的话。5.2 长期维护比一次验证更花时间很多人在尝试形式化时低估了维护成本。前两天你写的证明能通过编译过了一个月你更新了一些依赖库或者是修改了一个底层定义原来的证明很可能就编译不过了。数学库的API会变某些引理的名字会重新组织这些都会让你的旧证明“过时”。我现在的做法是尽量把验证目标放在明确的、稳定的位置同时保持源文件尽可能“原子化”。也就是每个文件只做一件小事文件之间不要有太多偷偷摸摸的跨文件依赖这样即使某个证明坏了修复的范围也有限。另一个经验是遇到库升级导致的编译失败不要急着“绕过”先去查一下失败原因很多时候是库改进了某个引理的名字或条件只要同步改一下调用方式就行。这种“维护”本身也是在产出一个新的验证单元你修复一条证明系统里就多了一条更稳定的记录。用工程化的观点看这就是技术债务的偿还虽然不产生新论文但整个证明库的健康度会因此提升也会让别人更愿意信任和复用你的工作。5.3 如何把手写证明“翻译”进验证系统最后分享一个我个人很受用的方法翻译手写证明到形式化系统时不要试图一次性写完。先写出theorem的声明和大概的prove skeleton也就是主要步骤中间用sorry占位然后一个一个补上具体的策略每补一个就运行一次编译器。这个过程把一个大任务分解成许多自检的小任务每完成一个小任务确认编译通过整体的心理压力会小很多。纯数学上的推导和形式化证明之间本质上隔着两层第一层是把模糊的语义变成精确的语句第二层是把数学推理变成对策略的调用。很多新手卡在第二层但其实第一层才是真正的价值所在。如果遇到翻译困难往往不是你不会用一个策略而是你还没想清楚“这个断言到底在说什么”——那就先放下代码回到草稿纸上重新理一下数学。另一个小技巧是善用Lean的#check命令。每当你写了一句新的定义或引理先用#check看看它的类型确认它确实是你想要的那个对象。这个习惯能帮你快速发现类型错误和定义偏差省掉很多调试时间。6. 常见问题速查与个人心得6.1 问题速查表这张表总结了我自己在实际使用形式化验证和进行大规模证明管理时遇到过的一些高频问题以及对应的处理思路方便大家遇到类似情况时快速对上号。现象可能原因我的常用处理办法编译时提示unknown constant依赖库没有导入或者定义名拼写有误用#check查看环境中是否存在该常量证明目标无法合流主策略用错或不满足先决条件拆开目标先做结构归纳再交给自动化策略维护旧证明时编译失败底层库变化引理改名或条件调整查看失败的定位信息同步更新调用方式形式化翻译卡住数学定义不够精确回到草稿手写出更详细的步骤证明过程太慢单个文件依赖过重拆分文件缩小验证范围数学库找不到想要的定理搜索关键字不对用库内搜索如grep或#find按模式匹配6.2 数学出版和评价体系的滞后写到这里我想顺带提一个比较现实的问题现在的学术评价体系还没有完全跟上“证明丰裕”的节奏。很多单位在评估科研人员时看的仍然是论文数、期刊档次、引用量。你贡献了几十条被几百个后续工作依赖的重要引理在现有指标里可能得不到任何直接体现这确实是一件让人遗憾的事。但抱怨归抱怨我自己的心态是好工作是能被识别出来的。就算当前的评价指标有滞后只要你产出的证明对象足够可靠它有朝一日一定会帮助你建立起口碑。我认识的几位同行职级晋升材料里没有那么多“豪华”论文但他们维护的证明库却被整个小圈子依赖着这样的人在同行评审里通常不会吃亏。所以哪怕外界评价暂时不敏感把精力花在提高工作的可复现性和可靠性上长期来看仍然是值得的。6.3 给研究生和新入门者的几条具体建议如果你还在读研究生或者刚开始接触数学研究我给几条比较具体的建议不一定全面但都是我实践中验证过有效的第一第一学期就把版本管理工具用熟。很多数学系学生不习惯用git等毕业论文写到一半才发现引理版本乱了那时候再补救就晚了。第二至少学一学数学库查找技巧。我不管你是用Lean、Coq、Isabelle还是只做数值模拟学会高效检索已知结果能省掉大量重复劳动。第三在正式写大论文之前先做几个小验证单元练手。就比如上面那个偶数的例子由简到繁你的肌肉记忆会慢慢建立起来。第四不要把形式化验证看成额外的负担把它当作另一个“听众”。这个听众极其严格它听不懂“显然”也不会被你华丽的修辞打动但它能保证你最后交付的是一个结构真正无懈可击的对象。跟它打交道越久你越会觉得人肉证明的那种“模糊地带”其实是危险的。就我个人这几年的体验而言最好的数学工作状态是既能在抽象层面自由地想又有精确的系统在身后兜底。“证明的丰裕”看起来增加了我们的负担但同时也让整个领域的信任基础变得更牢固了。刚开始做验证的那几个月我经常被工具的细节折磨到怀疑人生但坚持下来之后这种“每个结论都有据可查”的踏实感让我很难再回到过去那种靠记忆和感觉支撑的工作方式。希望这个分享能帮你少走一点弯路也欢迎你在实践之后回来讨论自己的体会。