Lean 证明了什么，又没有证明什么

我为什么需要 Lean

在 MRI 项目里，我面对一个很直接的困境：我不懂 MRI，也不懂其中大量数学，代码和证明主要由 AI 完成，我凭什么相信它？

我当然可以让另一个模型审查第一个模型，也可以让它们反复辩论。但如果最后仍然由一段自然语言告诉我“证明没有问题”，我只是把信任从一个模型转移给了另一个模型。

我也可以寻找领域专家。至少在今天，专家对于检查问题有没有被翻译错、结论是不是早已存在、抽象模型是否遗漏了决定性的物理条件，仍然不可替代。但如果 Auto Research 成立，AI 产生逻辑命题的速度和数量最终可能超过任何人逐项阅读的能力。专家不能永远成为每一项推导的人工签字员。

我需要的是一套机制，让我不必假装自己看懂了每一步，也不必要求某个人替我担保全部结果。

Lean 在项目中的位置由此出现：

逻辑问题不以“有人觉得证明合理”为终点，而以形式系统完成机械检查为终点。

这并不意味着 Lean 比数学家更懂 MRI。它根本不懂 MRI。它只是把“这句话能不能从那些前提推出”，从一种阅读判断变成一个能够由小型内核重复执行的检查。

Lean 检查的不是论文，而是形式对象

自然语言证明允许省略。作者会写“显然”“同理可得”或“经过简单计算”，读者用自己的知识填上中间部分。AI 尤其擅长生成这种看起来连贯的推导：每一句都很像数学，句子之间却可能缺少真正的逻辑连接。

Lean 不接受“看起来”。

一个命题进入 Lean，至少要被拆成几样东西：

定义：讨论的对象究竟是什么
假设：允许使用哪些前提
结论：究竟要证明哪一句话
证明项：结论怎样由定义、假设和已有定理构造出来

Lean 的内核检查证明项是否真的具有目标命题所要求的类型。检查通过，意味着在已经形式化的世界里，这条推导闭合了。

它没有阅读论文摘要，也没有理解作者“本来想说什么”。自然语言里相邻的两句话，如果没有被写成形式关系，在 Lean 中不会因为它们听起来顺畅就自动连在一起。

所以，形式化首先不是把一个结论变得更宏大，而是把它变得更窄、更具体。

Lean 证明的永远不是笼统的“MRI 是这样”，而是：对这里定义的对象，在这些明确假设下，这个精确结论成立。

一个有限但真正被证明的例子

MRI 项目曾经研究一组多壳 HARDI 的相位耦合候选。

最初的工程观察是：改变某些相位以后，数值扫描得到的谱指标似乎没有变化。但再多有限次扫描，也只能说明这些配置没有出现差异，不能推出所有允许的相位模式都必然如此。

于是问题被改写成一个逻辑命题：在项目定义的有限维 sheaf 模型和这组特定的相位耦合族中，候选 E 与候选 C 是否通过一个酉变换关联，从而具有相同的 sheaf bandwidth？

Lean 中最终建立的是这样一条受限结论：

对形式模型允许的任意相位模式，两个候选的 sheaf bandwidth 相等。

它把有限次没有发现差异的数值观察，推进成了该形式候选族内的普遍结论。这里的“任意”不是来自多跑了一些样本，而是来自证明对变量本身成立。

但这条定理没有证明：

• 所有 MRI 相位耦合都没有价值；
• 任意非酉耦合也保持同样的谱性质；
• 真机上的噪声、硬件误差和序列约束不会产生其他效果；
• 这套 sheaf 表达就是 MRI 的唯一正确表达。

它关闭的是一个被精确定义的候选族中的一条路，不是整个 MRI 领域中的所有路。

这正是形式化的力量，也是它的边界：它可以把一个小结论钉得很牢，却不会替作者偷偷扩大结论的适用范围。

“唯一恢复”究竟是哪一种唯一恢复

另一个例子更容易被误读。

项目在一个有限维 HARDI 采样模型中形式化了这样的关系：零阶上同调消失、采样算子的核为零、采样算子是单射，这几种表述在相应定义下彼此关联。通俗地说，在这个抽象模型中，不存在两个不同的系数向量产生完全相同的测量结果。

这可以被简称为“唯一恢复”。

但如果只看到这四个字，很容易把它扩写成“Lean 证明了 MRI 可以唯一恢复”。那就错了。

形式模型里的有限维信号空间、测量方式和采样算子已经被定义好。Lean 在这里证明的是：零阶上同调消失，恰好等价于这个采样算子是单射；这条等价本身没有先假定满秩。只有另外讨论 sheaf bandwidth 的正性和奇异值比时，才需要非零维、最小奇异值为正，也就是相应的满列秩条件。

这些定理都没有证明一台真实扫描仪满足形式模型的条件，没有处理所有噪声和模型误差，也没有证明有限维表示足以包含真实组织中的全部信息。

更不能从中推出某个临床扫描一定可靠。

同一句“唯一恢复”，可以位于完全不同的现实层级：

抽象有限维算子中的单射
≠ 数值实现中的稳定重建
≠ 体模或真机上的可恢复性
≠ 临床任务中的有效性

Lean 只结束其中被形式化为逻辑问题的那一层。后面的层级如果要成立，各自还要被写成工程问题，在相应现实条件下完成复现。

lake build 通过意味着什么

这个项目给形式轨设置过几个很硬的表面标准：lake build 通过，代码中没有用 sorry 或 admit 留下未完成证明。

sorry 和 admit 可以暂时让 Lean 接受一个还没有真正完成的证明。在探索阶段，它们可以是占位符；在宣布逻辑命题已经立住时，它们不能继续存在。

我重新运行当前 MRI 形式库时，没有只构建基础框架，而是显式加入本文使用的两个 DWI 目标：

lake build MRI DWI.HARDIBandwidth DWI.HARDIMultiShell

这次构建完成了 8328 个任务。输出里有一条代码行超过 100 字符的风格警告，但没有证明失败。项目的 Lean 源码中也没有实际使用 sorry、admit 或自行声明的 axiom。

这些检查能够说明：

• 当前版本可以由现有 Lean 与 mathlib 环境完整构建；
• 已声明完成的证明没有用占位符跳过缺口；
• 证明项通过了 Lean 内核的类型检查。

但“零占位符”仍然不等于“零前提”。形式证明总是在某套定义、公理、已有定理和软件实现上运行。某个定理具体依赖哪些公理，需要继续检查它的公理依赖；Lean 内核、编译器、mathlib 和构建环境本身也组成了需要信任和治理的计算基础。

形式化不是消灭信任，而是把一大片难以审查的自然语言推导，压缩到更小、更明确、可以反复检查的可信边界。

Lean 没有检查写进去的是不是正确问题

这是最重要的限制。

Lean 会严格忠于实际写进系统的定义，而不是忠于我脑中的意图，也不是忠于 MRI 世界本身。

如果 AI 把“采样”“可恢复性”或“物理对应”翻译错了，Lean 仍然可能完美证明翻译后的命题。此时形式推导没有漏洞，研究却可能从第一步就走偏。

它至少不能替我完成以下判断。

第一，语义是否忠实。自然语言、教材概念和形式定义之间有没有发生偷换？

第二，前提是否适合现实。教材和论文提供的是当前知识底座，不是不会被修正的宇宙公理；为了可证明而加入的理想条件，也可能在现实中根本不满足。

第三，工程是否真的发生。定理不能替代程序运行，更不能替代真机、体模、独立数据或临床实验。

第四，结果是否新颖和重要。一个定理可以完全正确，却只是已知结论的实例、定义的展开，或者不改变任何预测与决策。

第五，形式化范围是否足够。MRI 仓库明确没有形式化完整的范畴论包装、三个物理对应和经验性命题。没有进入形式系统的部分，不会因为旁边的 Lean 文件通过了构建就自动获得证明。

因此，“Lean 已验证”必须跟着一个范围说明。缺少范围的形式化标签，也可能成为另一种权威修辞。

Lean 不是领域专家的替身

如果 Lean 不能判断语义和现实，那是否仍然需要专家？

今天当然仍有价值，但这不等于当前每项结果都要把专家签字作为成立前提。

专家可以发现一个定义虽然自洽，却没有表达领域真正关心的对象；可以认出所谓新结论只是常识；也可以指出模型遗漏了哪个物理约束。Lean 不具备这种由长期实践形成的领域判断。MRI 项目当前已经完成的形式命题和软件层复现，并没有以专家逐项签字为前提；专家更重要的位置，是尚未完成的语义审查、物理映射和现实世界的最后一公里。

更可扩展的分工可能是：专家参与建设和审计语义接口，规定哪些现实条件必须进入模型，抽查异常与高风险结果；形式系统批量裁决已经进入逻辑轨的命题。人负责规则、边界、价值冲突和现实接口，不再假装能够阅读无限增长的全部推导。

同样，形式系统也必须被治理。版本要锁定，依赖要记录，公理要审计，验证器发生变化时要重新评测。不能一边主张人无法逐项验证 AI，一边把验证器本身当成永远不会出错的神谕。

Lean 不是把“相信专家”换成“相信软件”。它的意义在于把不同责任拆开：逻辑闭合由内核检查，语义对应由领域知识和规格治理，工程事实由现实复现，价值选择由目标和资源约束决定。

它没有消除我的无知，而是把无知分层

在 MRI 项目开始时，我希望找到一条边界：当我无法亲自审查 AI 的全部成果时，究竟还能保证什么？

Lean 给出的答案比“AI 证明了一个 MRI 定理”窄得多，也有用得多。

我可以作出一个更窄的声明：某个精确命题已经被写入形式系统；在公开的定义、假设和依赖下，它的证明项通过了机械检查。我也可以明确标出：从领域语言到形式定义的翻译还可能错，模型和软件层虽然已有部分工程复现，真机、体模与临床层的现实验证仍未发生，原创性与意义也没有因此自动得到回答。

这不是完整真理。

它是一张不会把不同未知混在一起的地图：

这里，逻辑已经闭合
这里，语义仍待审查
这里，模型和软件层已有部分复现
这里，真机、体模与临床证据还不存在
这里，价值仍需判断

对于 Auto Research，这种分层比一张“验证通过”的总印章更重要。系统可以因此知道哪些问题已经走到自己的终局，哪些必须停留在边界，哪些需要被送往另一条轨道或另一种治理机制。

Lean 没有证明我理解了 MRI，也没有证明 MRI 项目整体正确。

它证明的是一件更朴素的事：在一个被明确写下来的形式世界里，我们没有仅仅因为一句话听起来像证明，就把它当成证明。