AI 研究狂飙的时代，为什么形式化会变得更重要
这几年 AI 研究的节奏明显变了：模型能力、工具链、论文、开源项目、benchmark 和应用场景都在高速迭代。很多过去需要专家慢慢写、慢慢查的东西，现在可以由模型在几分钟内生成一个看起来很像样的版本：代码、实验计划、定理证明草稿、综述、数据分析、系统设计，甚至新的 conjecture。
这当然是巨大的生产力提升。但它也带来一个更尖锐的问题：当生成速度远远超过人工验证速度时，我们到底靠什么维持可信度？
形式化的重要性，正是在这个背景下突然变得现实起来。
AI 让“产生候选答案”变得便宜，形式化让“确认答案真的成立”变得可机械检查。未来很多关键知识工作，会越来越依赖这两者的组合：AI 负责搜索和生成，形式化系统负责约束和验收。
什么是形式化
形式化并不是把数学或程序写得更“像代码”而已。它的核心是：把一个命题、规范或证明，写进一个有精确定义的逻辑系统里，让计算机可以逐步检查它是否真的成立。
以 Lean 为例，我们可以把自然数、函数、群、环、拓扑空间、测度、范畴等对象都定义在系统中，再把证明写成 Lean 可以检查的项。Lean 的 kernel 不会因为一句“显然”就放行，也不会因为作者很有名就默认正确。它只做一件事：检查这个证明项是否真的具有目标命题对应的类型。
所以形式化证明的意义不是“让电脑相信人类”，而是把证明变成一个可以被独立检查、可以被复用、可以被组合的 artifact。
传统论文证明是面向人类阅读的文本；形式化证明则更像面向机器和人类共同使用的知识对象。
AI 时代的问题不是没有答案，而是答案太多
在 AI 辅助研究之前，很多领域的瓶颈是“想不出方案”或“写不出草稿”。现在情况正在变化：模型可以一次给出十几个证明路线、几十个代码实现、上百个实验变体。问题开始从生成侧转移到验证侧。
这会产生几个典型风险：
- 幻觉变得更难发现。 模型生成的文本越流畅，越容易把缺失条件、偷换定义、错误引用藏在顺滑叙述里。
- 局部正确不等于整体正确。 一个证明片段看起来没问题，一个程序函数测试通过，都不能保证完整系统满足目标性质。
- 研究链条越来越长。 AI 生成的中间结论如果没有可靠记录和检查，后续工作会在不稳固的地基上继续堆高。
- 人工 review 速度跟不上。 人可以抽查，但很难持续审完机器每天生成的大量候选产物。
这不是说 AI 不可靠，所以不能用。恰恰相反：AI 越有用，我们越需要一种机制，把它生成的结果接到可靠的验收层上。
形式化就是这个验收层的重要候选。
形式化把“看起来对”变成“检查通过”
人类推理里有大量隐含上下文。数学家写“由紧性可得”，通常默认读者知道使用的是哪个紧性定理、空间满足哪些条件、映射在哪个拓扑下连续。软件工程师写“这个状态不会出现”，通常也默认了某些调用顺序、输入约束和并发假设。
AI 很擅长模仿这种写法，但它不一定真的持有那些隐含条件。
形式化系统会把这些隐含条件全部逼出来：
- 定义必须明确；
- 前提必须列出；
- 类型必须匹配；
- 引理必须已经证明；
- 每一步推理必须能被 kernel 检查。
这会让人一开始觉得繁琐，因为许多“人类觉得显然”的地方都要补全。但在 AI 高速生成的场景里，这种繁琐反而是价值所在：它把模糊的自然语言说法，转化成能被机器反复检查的精确结构。
可以说，形式化不是为了降低表达成本，而是为了降低长期信任成本。
Lean 的角色：数学知识的编译器
Lean 是今天最受关注的证明助手之一，尤其因为 mathlib 已经积累了大量现代数学基础库。它可以表达复杂的数学结构，也可以把定理、定义和证明之间的依赖关系组织成一个可搜索、可复用的库。
如果把传统数学论文看成“自然语言源码”，那么 Lean 形式化有点像给数学加上编译器：
- 定义不一致，编译不过；
- 条件缺失，编译不过；
- 引用的定理不适用，编译不过；
- 证明跳步，编译不过；
- 依赖关系可以被系统追踪。
这对 AI 特别关键。因为 AI 可以生成 Lean 代码，也可以尝试补证明；但最终能不能进库，不由模型自己说了算，而由 Lean 检查。
未来理想的工作流可能是这样的：
- 人类提出问题、定义和研究目标；
- AI 生成候选证明、相关引理和搜索方向；
- Lean 检查每个候选 proof artifact；
- 通过检查的部分进入知识库；
- 新知识再被后续 AI 和人类复用。
这个循环的关键不是“AI 是否聪明到永远不犯错”，而是“AI 犯错时能不能被低成本、系统性地拦下来”。
形式化会改变 AI for Math 的评价方式
AI for Math 很容易被漂亮的 demo 吸引：模型解出一道题、生成一段证明、发现一个路线。但数学研究真正需要的是可积累的可靠知识，而不只是一次性答案。
形式化系统提供了一种更硬的评价方式：
- 证明是否通过 checker；
- 是否使用了额外公理；
- 依赖了哪些库和引理；
- 是否能在新版本库中复现；
- 是否能被后续定理复用。
这比“看起来像证明”强得多。它也让 benchmark 从自然语言评分，转向 proof artifact 评分。模型不只是要说服评测者，而是要产出一个可以被 kernel 接受的对象。
当然，checker 也不是神。形式系统本身、kernel 实现、库定义、问题建模都可能有边界和漏洞。但即便如此，形式化仍然把信任边界大幅收窄了：我们不再相信一整段自然语言推理，而是主要相信一个小得多的 kernel、清晰的定义和可审计的依赖链。
不只是数学：软件、硬件和协议更需要它
形式化的价值不只在数学。AI 正在越来越多地写代码、改系统、生成配置、设计协议。普通测试只能说明“这些样例没坏”，但很多关键错误只会在极端状态、并发交错、安全边界或长期演化中出现。
形式化方法可以表达并检查更强的性质，例如：
- 编译器优化是否保持程序语义；
- 加密协议是否满足认证和保密性质；
- 智能合约是否不会在某类调用下丢资产；
- 分布式系统是否满足一致性约束；
- 控制系统是否不会进入危险状态；
- AI 生成的代码是否满足给定 specification。
随着 coding agent 变得更强，软件生产会更快，也会更容易出现“看起来能跑，但没人真正理解完整行为”的系统。形式化规范和验证工具会成为抵消这种风险的基础设施。
未来的高可靠工程里，AI 可能负责写实现、补测试、找反例；形式化工具负责定义不可妥协的边界：哪些状态不允许发生，哪些性质必须保持，哪些优化不能改变语义。
形式化也是一种知识组织方式
还有一个常被低估的点：形式化不仅是在“证明正确”，也是在重新组织知识。
自然语言知识库很适合阅读，但不擅长自动组合。一个定理能不能用于另一个场景，往往要专家自己判断。形式化库则把定义、实例、类型类、定理依赖都结构化了。它让机器知道：这个对象是什么类型，满足哪些性质，可以调用哪些定理，还缺哪些前提。
这对 AI 很重要，因为模型需要的不只是更多文本，还需要更可靠的工具环境。一个大型形式化库相当于给 AI 提供了一个高精度的知识图谱和操作空间。模型可以在其中搜索、尝试、失败、修正，而不是只在自然语言相似性里游走。
换句话说，形式化让知识从“可读”进一步变成“可计算”。
最大障碍：成本和体验
如果形式化这么重要，为什么还没有成为主流？主要原因也很直接：成本高。
形式化一段数学证明，往往比写论文证明更费时。形式化一个工程系统，也需要提前定义 specification、抽象模型和不变量。对初学者来说，Lean、Coq、Isabelle、TLA+、Dafny、F* 等工具都有学习曲线。
这也是 AI 可能反过来帮助形式化的地方。过去形式化最贵的是细节劳动：找定理、补类型、处理繁琐的 rewrite、把人类证明拆成机器可接受的小步。AI 如果能承担其中一部分，就会显著降低形式化门槛。
所以 AI 和形式化不是对立关系。更可能出现的是互补：
- AI 降低形式化的书写成本；
- 形式化降低 AI 输出的信任成本；
- AI 扩大可形式化的范围；
- 形式化筛选真正可靠的 AI 产物。
这是一种正反馈。
未来重要的不是“全自动证明”，而是“可信流水线”
很多讨论会把目标想成：AI 什么时候能完全自动证明所有定理？这个问题当然有趣，但可能不是最先改变世界的部分。
更现实、更重要的变化，是可信流水线的形成：
- 需求用更清晰的 specification 表达；
- AI 根据 specification 生成实现或证明；
- 工具自动检查类型、性质、反例和依赖；
- 人类审查抽象是否合理、目标是否值得、模型是否贴近现实；
- 通过检查的 artifact 被纳入可复用库。
这条流水线不会消灭人类判断。相反，它会把人类从大量机械验证里释放出来，把注意力放回建模、抽象、问题选择和概念创造上。
结语
在 AI 研究快速发展的时代，我们最不缺的是生成能力。模型会越来越会写，越来越会猜，越来越会组合已有知识。真正稀缺的是可验证性：哪些结果能被信任，哪些结论能被复用，哪些系统能在关键场景里承担责任。
形式化的重要性正在于此。
Lean 这样的证明助手，形式化验证这样的工程方法，不只是学术上的严谨爱好。它们可能会成为 AI 时代的基础设施：像编译器检查程序一样，检查证明、规范和推理；像类型系统约束代码一样，约束机器生成的知识；像版本库记录代码演化一样，记录可验证知识的积累过程。
AI 让我们更快地产生可能性。形式化帮助我们分辨哪些可能性真的站得住。
未来的关键不是在二者之间选一个，而是把它们接在一起。