从AI攻数学到大模型发展卡点(5/8)形式化证明:Lean 革命
把数学翻译成能编译的语言。编译通过即定理成立——信任的载体从人变成内核。
接上篇：之四说信任成了商品，这一篇看铸币厂——Lean，一台把"我相信"熔炼成"可核验"的机器。
PART 01 Lean 是什么：数学的编译器
Lean 是一门定理证明语言：命题写成类型，证明写成程序，内核逐行做类型检查。它的本质是把"同行评审"这个由人承担的社会流程，变成一个几百行内核代码就能完成的机械过程。编译通过 = 定理成立，不需要信任任何人。围绕它长出了数学界的"标准库"mathlib——数十万条已形式化的定义与定理，是所有新工程的公共地基。
形式化流水线：从自然语言命题到可复用引理库，每一步都有机器把关
PART 02 里程碑：从 PFR 到费马大定理
形式化的生产力曲线在三年内被彻底改写。2023 年陶哲轩的 PFR 项目：社区众包 + Lean 判卷，三周形式化一篇新论文。2024 年 Equational Theories 项目：2200 万个等式蕴含关系，AI 写、Lean 验、全球志愿者认领，57 天基本完成，还催生了新概念。2026 年 9 月，Claude 用 11 天、约 60 亿 token 完成费马大定理的端到端形式化：1300 万行 Lean 代码、3 万余个辅助定理，只靠三条标准公理，Buzzard 等参与核验——人类史上最著名的定理，第一次从头到尾跑在机器里。
PART 03 生态地图：三条技术路线在赛跑
- 神经符号流水线（DeepMind / Harmonic / Kimi 等）：模型生成战术，符号内核兜底，专门的 prover 模型（如 Leanstral 这类"为 Lean 而生"的小模型）打配合；
- 单模型长跑（Anthropic 路线）：一个模型连续工作数天，靠上下文与自我纠错啃下巨型工程；
- 多智能体并行（OpenAI 路线）：数十到上万个子智能体分工探索，汇总裁决——ζ 零点下界就是约 60 个子智能体、3100 万 token 的产物。
配套的"公共登记处"也在出现：数学家开始维护 AI 成果的核验注册表（如 Palomar 式的登记簿），谁的结果通过了内核、谁只是宣称，一目了然。制度的空白正在被社区自发填上。
撞车现场：如果你觉得"数学应该能编译"——恭喜你，你和德布鲁金想到的一样：他 1967 年创造的 Automath 是第一个机器证明检查系统，比个人电脑还早。Lean 是这个五十年梦想的成年版。
施工图：入门路径今天完全开放——装 Lean，跟着 mathlib 的教程形式化一条你熟悉的定理，你会在第一个周末就理解为什么数学家说这"像打游戏一样上瘾"。
PART 04 暗面：形式化的三宗罪
革命叙事之外，得给 Lean 摆上三个诚实的罪名。其一，形式化 ≠ 理解：一个证明编译通过，只保证它合法，不保证它有趣——就像一篇语法全对的作文可能毫无内容。1300 万行 FLT 代码里，人类真正"读懂"的比例恐怕不高；机器证明了定理，人类还要再等一个能讲出"为什么非得这样证"的读者，无论那个读者是人是机。其二，成本依然陡峭：形式化一行纸面证明，经验上要花五到十倍的篇幅；60 亿 token 换费马大定理，是壮举也是价格标签。其三，意义漂移：把自然语言命题翻译成类型时，翻译本身可能悄悄换掉命题的魂——A 证明了"某个性质的形式化版本"，而那个版本是否还是原来的问题，仍需人来裁决。编译器保证推理的忠诚，不保证翻译的忠诚。
一次十一天的长跑，烧出的三个天文数字（对数刻度）
PART 05 五十年的伏笔：为什么是现在
Lean 的故事里藏着一条对年轻人最有用的经验：基础设施的回报周期以十年计，但拐点来的时候毫无预兆。1967 年德布鲁金造 Automath 时，被同行当作怪癖；2013 年 Lean 立项时，只是微软研究院的一个工具项目；mathlib 社区滚了十年雪球，才在 2023 年后突然被 AI 点燃——因为模型需要的从来不是"更深的数学"，而是"已格式化的数学"。那些年里默默形式化定理的人，当时看是在做慈善，事后看是在铸造货币。人生里大多数值得做的事都长这样：在没人鼓掌时铺路，在所有人涌来时任他们踩。
工程现场："能编译的规格"在制造业早就有，叫 GD&T（几何尺寸与公差）：一张图纸上的公差标注是形式语言，三坐标测量机是内核，检测报告是编译结果——机器判合格，不需要信任任何人。功能安全标准把这条推到更深处：汽车 ISO 26262、工业 IEC 61508 要求高安全等级的控制逻辑必须用形式化方法验证——刹车的控制代码，早就在过 Lean 式的生活了。而"翻译忠诚"问题在工厂天天上演：客户图纸上的一个公差标注被车间误读，和命题形式化时的意义漂移是同一种事故。差别只在赔偿方式：工厂赔批次，数学赔声誉。
散记：数学家花三百年追求"严格"，最后发现严格的尽头是一台编译器。这不讽刺——就像诗人追求一生的格律，最后是为了在破律的那一刻掷地有声。思考题：如果你的工作成果都能被"编译检查"，你的行业会有哪些岗位消失、哪些岗位诞生？
下一篇预告：内核能判对错，却不能给训练"发工资"——判定是一次性的，而学习需要持续的奖励流。验证如何变成奖励、奖励如何长出推理能力？下一篇是这个系列的技术心脏：RLVR。
我是过海，产业转型观察者，产业学院陪跑人。