从费马大定理看Lean 4与AI文风：机器校验的可信度

如果你平时关注形式化验证，最近应该被一条消息刷屏了：Anthropic 放出了一个基于 Lean 4 的费马大定理机器校验证明，Ethan Mollick 很快指出，整份文档明显带着 Claude 文风。这条消息有意思的地方，不在于“AI 又证明了某个定理”这种标题党式解读，而在于它把两个热点焊在了一起：一边是 Lean 4 这门发展了多年的交互式定理证明工具，另一边是大模型生成文本的可辨识性。这两件事放在一起看，信息量远超“定理本身”。

我做程序语言和自动定理证明有些年头了，也亲眼看着大模型从“写代码还行”进化到“能帮着写数学证明”，所以这次事件里我最关注的，其实不是证明本身长什么样，而是 Ethan Mollick 点出来的那个细节：“文档仍带有 Claude 文风”。这意味着什么？意味着那份文档很可能是人机协作的产物——机器负责补证明脚本，人类负责把关逻辑，但 AI 的表达习惯还是渗透进了注释和整体结构。这份观察非常精准，也带出了一个更值得聊的话题：当一项以“消除人类主观瑕疵”为目标的机器校验证明，自己身上也带着 AI 印记时，我们该怎么看待这份证明的可信度。

这篇我会把整个事件拆开讲：先聊费马大定理和 Lean 4 为什么能搭在一起，再讲 Lean 4 的实际使用原理和几个实操要点，接着分析“Claude 文风”到底是怎么混进严谨数学文档的，最后总结一些避坑经验。无论你是研究数论、在用 Lean 写证明，还是纯粹好奇“人类内容与 AI 内容的边界”，这篇都值得继续看。

1. 事件拆解：为什么一份“机器可读”的费马大定理证明会引起如此关注

1.1 费马大定理为什么是形式化验证界的目标

费马大定理在数学界的地位不用多说。1637 年费马在《算术》书边写下那句“我确信已发现一种绝妙的证法，可惜空白太小写不下”，之后三百多年无数数学家栽在它上面，直到 1994 年怀尔斯才给出严密证明。这一定理单独看是一个数论命题，但它背后牵连的工具太多——椭圆曲线、模形式、伽罗瓦表示，全部串在一起，中间任何一环有漏洞，整个证明就白搭。

很长一段时间里，研究者都把“把怀尔斯证明形式化”看成一件可以写进理想清单、但很难真正落地的任务。因为 Lean、Coq 这类证明助手要求的是完全结构化的、机器可校验的证明树，而怀尔斯的原始证明用人脑读都非常吃力，更别提让机器逐行确认。所以 Lean 社区早先把“费马大定理形式化”列为长远目标时，很多人是抱着“慢慢来、先积攒基建”的态度。

这也是为什么 Anthropic 的这次上传会引起关注。如果一份基于 Lean 4 的费马大定理证明真的能通过内核校验，那说明两件事：第一，Lean 的数学库 mathlib 在过去几年里积累的底层结果，已经足以支撑这种级别的难题；第二，AI 在“把自然语言证明翻译成可被机器校验的证明脚本”这件事上，已经能真正干活了，而不只是生成一些看起来像样的 LaTeX 片段。这两件事任何一件单独出现都够热闹，合在一起就是一次标志性事件。

1.2 Anthropic 与 Lean 4：AI 公司参与定理证明的动机

Anthropic 是 Claude 的开发商，它搞这个项目，当然不纯出于数学情怀。从公司战略角度看，让模型参与大规模形式化证明有非常明确的收益：形式化证明是“可验证推理”的终极场景。写代码可能有隐藏 bug，写文章可能有幻觉，但 Lean 4 环境里一条定理能编译通过，就说明逻辑链路闭合了——这在维度上已经高于平时说的“模型正确性”。

我个人的理解是，Anthropic 不只是想证明 Claude 能做题。它更想验证的是：Claude 能不能作为“AI 数学家”和人类研究者一起工作，把人类用自然语言写出的数学想法，逐步转化为 Lean 4 可以接受的严格证明。这条路如果走通，未来大模型就不只是“生成建议”，而是真的能作为研究伙伴，参与审查、补全、扩展各种证明。

另外还有一个更现实的动机：Lean 4 本身是可控推理平台。模型参与 Lean 证明时，每一步 tactic 都有明确的上下文和合法目标，模型不能瞎编，否则编辑不过。这种环境下产生的失败信号、成功信号，对训练模型非常有价值。所以这次项目更像一次实验数据收集，而不是单纯的炫技。

1.3 Ethan Mollick 的观察：文风成了“数字指纹”

Ethan Mollick 是沃顿商学院教授，长期观察 AI 对人类工作的影响。他这次指出的点非常敏锐：哪怕一份严谨到不行的 Lean 4 证明文档，字里行间还是能看出“这是 Claude 写的”。这句话一出，很多人才反应过来——对，我们一直在讨论 AI 能不能做好数学，却忽略了 AI 参与过的文本本身就自带一个可识别的“数字指纹”。

为什么这值得注意？因为 Lean 证明文档主要由公式和策略调用组成，按理说已经是“最没风格”的文本类型。如果你连这种文档都能看出 AI 文风，那说明大模型生成文本有一个挥之不去的指纹层，它不受任务内容影响，而是由模型训练数据、标注偏好、系统提示习惯共同塑造的。这就像一个人说话再克制，口音还是藏不住。Ethan 的意思不是“AI 写不好证明”，而是“AI 的参与痕迹近乎无法消除”——这本身就是很好的研究素材，也是每个在用 AI 辅助工作的人都应该正视的现实。

2. Lean 4 形式化证明：不是写代码，是“教机器懂数学”

2.1 Lean 4 到底在做什么

往简单里说，Lean 4 是一个交互式定理证明器。你给它几个公理、几个定义，它通过一套类型系统和归纳构造演算，把“命题就是类型，证明就是构造该类型的项”这个思想做到极致。你的目标不是写程序，而是构造一个满足指定类型（也就是命题）的证明项。听起来玄乎，拿加法举例：

命题“2+2=4”在 Lean 里被表达成一个类型，你要做的不是喊“显然等于 4”，而是给一个证明项，让 Lean 的 kernel 一层层检查这个项的每一步推导是否合法。如果检查通过，机器才承认这个命题为真。

我见过很多程序员第一次接触 Lean 4 的反应：这不就是写代码吗？其实差别很大。写普通代码的目的是让机器执行任务，写 Lean 证明的目的是让机器验证逻辑。代码可以写出 bug 然后慢慢修，Lean 证明则要求从公理到结论的每一步都没有缝隙。这也意味着传统编程里的“跑一下看结果”直觉在 Lean 里会失效：你不能靠试运行来判断对错，你得证明自己的每一步推理成立。

2.2 一个最小示例：从命题到证明脚本

空谈原理没什么感觉，直接来一段最小示例。假设你要在 Lean 4 里证明加法交换律的一个特例：

import Mathlib example (a b : Nat) : a + b = b + a := by omega

这段代码看起来像程序，但它实际是一个“证明脚本”。example提出命题，by omega是让 Lean 调用 omega 决策过程自动完成自然数上的线性算术证明。Omega 背后是 Presburger 算术的决策算法，它能在有限步骤内判定这类等式的真假。

如果不用 omega，还可以写一个更直观的化简式证明：

example : 2 + 2 = 4 := by norm_num

norm_num的作用是直接对数值表达式求值并化简。两条代码走完全不同的路径，但最终都会得到同一个结论：在 Lean 4 的 kernel 看来，证明成立。对新手来说，最该理解的一点是“by后面那一长串 tactic 不是给人看的，是给内核检查的证据生成脚本”。如果你希望证明更容易人读，可以改用calc块：

example (x y : Nat) : (x + y) ^ 2 = x^2 + 2*x*y + y^2 := by ring

ring策略处理半环上的多项式等式。每个策略都封装了一批底层推理规则，策略成功后，Lean 会把证明项展开交给内核校验。

所以所谓“Lean 4 证明”，本质上是一棵树：叶节点是公理和已知定理，内部节点由 tactic 生成，根节点是你要证明的命题。树越大，证明越庞大。一份费马大定理级别的证明，不是几百行，而是几十万行、上百万行公式结构和经过精心组织的前置引理。

2.3 可校验证明的结构特征

Lean 社区把大型证明项目叫“证明开发”。它们一般有几个共同特征：

• 模块化：大定理被拆成许多小引理，每个引理独立可编译，编译过后可作为新的引理被后续使用。
• 高度依赖 mathlib：mathlib 是 Lean 社区的“标准数学库”，里面有大量代数、拓扑、数论结果。我自己参与的经验是，写证明的第一步经常是查 mathlib 里有没有现成引理，而不是自己从零写。
• 编译时间长：大型证明项目跑起来，经常要等几十分钟甚至几小时，因为 Lean 需要展开大量定义，校验大量由策略生成的证明项。

为什么费马大定理这种级别的东西需要机器校验？答案很简单：人类容易累、容易错、容易跳步。怀尔斯证明完 FLT 后，团队还花了一年多检查，最终修正了第一稿中的某些细节。这种“细节修正”在自然语言数学里很常见，但它意味着数学共同体一直靠“一群专家信任一个人”的链条运转。而 Lean 4 的机器校验，把信任链条换成了“逻辑可复现”。这不是说机器校验绝对没有坑，后面我会专门讲，但它至少提供了一条完全不同的验证路径：不再靠审稿人逐字读，而是靠编译器把它们忠实核对一遍。

3. 实操层面：用 Lean 4 做数学校验的关键环节与经验

3.1 项目组织：把大定理拆成可校验的中间结论

真正参与过大型 Lean 项目之后我才意识到，证明助手对你的“数学规划能力”要求，比证明技巧本身要高得多。费马大定理动辄上百个引理，如果上来就直奔主定理，大概率会在某个中间节点卡死。比较好的做法，是把整个证明分解成相互独立的部分。

我自己常用的分层思路是：先画出证明依赖图，列出哪个定理依赖哪几个定理、哪几个引理可以并行开发，然后按照叶子优先的顺序一个个推进。对于 AI 辅助场景，这一步更重要：给 Claude 或者任何辅助模型一个明确的中间目标，它生成可编译证明的成功率，远高于给它一个过于宽泛的“证明大定理”指令。

每个中间引理应尽量做到 self-contained，可独立编译。Lean 里建议用theorem显式命名并给注释，比如：

theorem flt_aux_one (a b c n : Nat) (hn : n > 2) (h : a^n + b^n = c^n) : a * b * c = 0 := by -- 这里是某个中间步骤 sorry

sorry在 Lean 里是一个危险的占位符，它告诉编译器“这步我暂时不管，你先放我过”。严格来说，带sorry的文件不算证明完成，因为它引入了未校验的公理。我在本地开发时常用sorry做骨架，但在提交前一定会全局搜索sorry并清零。这个习惯非常值得养成。

3.2 人机协作：AI 补证明与人工审阅的边界

这次 Anthropic 项目的重点，或者说任何 AI 辅助 Lean 项目真正的重点，是“人机协作的边界在哪里”。实际跑过你就会发现，Claude 这类模型在生成 Lean 4 代码时表现不弱，它知道大量 mathlib API，也能生成某些正确的策略序列。但它仍然会犯“看起来很合理但编译不过”的错误，而且错误往往藏在细节里——某个引理名字写错、某个隐式参数匹配不上，问题一多就非常磨人。

我的实操心得是：AI 负责“快速生成候选证明脚本”，人类负责“判断证明思路方向是否正确”。具体操作上，我会把要证的命题和已知可用的前置引理列表喂给 Claude，让它生成一个候选 proof，然后在 Lean 里编译。如果通过，就把这段脚本当普通代码做审查；如果不通过，先把编译错误贴回去让它修，实在修不动再人工介入重新规划思路。

这个流程的关键点是：永远不要把 AI 生成的证明直接当成最终证明。原因很简单，即使编译通过，也仍然要确认它没有引入axiom、unsafe这类绕过内核校验的手段。Lean 里有一条命令#print axioms my_theorem，能列出这个定理依赖的所有公理。如果一个所谓的 FLT 证明依赖了一个奇怪的额外公理，那它本质上不算证明，只是另起炉灶的假设。我建议所有做了 AI 辅助证明的人，提交前都跑一下这条命令。

3.3 版本与环境：复现一份 Lean 证明要踩哪些坑

形式化证明项目的可复现性，其实比很多人想象中更麻烦。Lean 4 的生态仍在快速演进，mathlib 的 API 时不时会调整，更别说策略实现细节对版本高度敏感。你今天能编译通过的证明，换一个 mathlib 版本，可能就因为某个引理被重命名或删除而编译失败。

这一点上，Anthropic 的公开上传有积极意义：既然文档已经公开，理论上其他人可以拉下来复现。但复现的前提是锁定版本。我在 Lean 社区看到的标准做法，是使用 Lake 项目工具配合lean-toolchain文件固定 Lean 版本和 mathlib 版本。lean-toolchain里写的是一个版本标签字符串，比如leanprover/lean4:v4.9.0-rc1。如果项目里没有这个文件，或者 toolchain 版本和你本地不一致，复现时大概率会陷入一堆奇怪的错误。

对想尝试的小伙伴，我的建议是：先找一个已经锁好版本的现成项目，而不是从零开始配。Lean 官方和 mathlib 社区提供了许多模板，把依赖拉齐之后再往里面加自己的证明文件，这样能把环境问题跟证明问题隔离，否则你很难判断到底是证明写错了，还是环境不兼容。

3.4 性能与编译时间的取舍

大型证明项目还有一个很实际的痛点：编译时间。Lean 的策略机制很强大，代价是编译时会生成大量中间项，规模稍大的文件，编译时间就会明显拉长。我自己见过一个项目，主文件一个by块里堆了二十多个策略，编译一次要几分钟，这在开发阶段非常痛苦。

经验之谈是，把长证明拆开：在关键节点用have声明中间结论，让每个have块都短小精悍，而不是一个巨型by一路到底。这样不仅能减少重复运算，还能让编译错误信息更具体，出错时定位更精准。逻辑上这跟写代码时的“小函数重构”很像：证明可读性变好，编译期更短，AI 辅助时也更容易分段指令。

另一个技巧是利用set_option maxHeartbeats 400000这类选项临时放宽编译资源上限，但这只是退路，不是首选。真正应该优先做的，永远是减少某一处策略块需要处理的信息量。

4. “Claude 文风”：AI 痕迹是怎么混进严谨文档的，以及我们要不要在意

4.1 什么是“Claude 文风”

Ethan Mollick 说“文档仍带有 Claude 文风”之后，很多人都在猜这句话到底指什么。所谓“Claude 文风”，不是一个具体的词，而是一组统计上很明显的表达偏好。Claude 这类模型经过大规模人类反馈对齐之后，倾向于使用清晰、有礼貌、总分总、并列递进式的表达。

如果你长期用 Claude，会发现它特别爱用这些词：“值得注意”、“重要的是”、“广义而言”、“综上所述”、“不仅……而且……”。它习惯在每一段结尾做正向总结，喜欢用破折号或冒号引入说明，还经常把内容分成小标题层层推进。这些都不是错误，甚至对可读性有帮助，但当一整份技术文档充满这种痕迹时，敏感的人一眼就能认出“这是 AI 写的”。

放到 Lean 证明文档中也是这样。数学证明的注释按说应该克制，但如果注释是 Claude 写的，它很可能每隔几行就总结一次“上述等式由此成立”，而不是像人类数学家那样只留下极简短语。文风就是这样的东西：在不需要谈风格的地方，它依然存在。

4.2 为什么形式化证明文档里也会出现文风特征

这里有一个很容易被忽略的点：Lean 4 的证明脚本本身并不需要太多自然语言注释。一份纯 Lean 的.lean文件，核心内容是策略调用和定义，理论上可以零注释。但现实中的项目文档，尤其是有 AI 参与的项目，往往会加入大量解释性文字——这些文字可能是给人类协作者看的，也可能是模型按系统提示要求，把工作过程记录得“详尽清晰”。

正因为如此，“Claude 文风”出现的位置很关键。它不在by块的核心策略里，而是散落在注释、README、pull request 描述、每个theorem上方的英文说明中。只要文档里有一处自然语言是 AI 生成的，且没有经过深度编辑，它的表达指纹就会保留。Ethan 能看出这点，恰恰说明整个项目的文档生成流程很可能高度依赖 Claude，而人类在验收证明时更关注逻辑是否编译通过，对文字风格基本没做审查——这是人机协作项目里很普遍的现象。

我们不能简单说这是坏事。文风相当于模型的品牌指纹，在可解释性上也有价值：当你知道某段解释是 AI 写的，就会自动提高警惕，去核实里面每条引理引用是否真实、每个论证是否完备。反过来，如果完全看不出来哪些内容是人写的、哪些是 AI 写的，反而更需要担心。

4.3 这是坏事吗：从“发现 AI 痕迹”到“人机协作新常态”

这次事件最值得讨论的地方，不在于“Claude 露馅了”，而在于它让我们意识到一个现实：AI 参与深度工作已经从“实验”变成了“默认”。项目文档、代码、甚至定理证明，都会被注入 AI 的表达习惯。将来我们判断一份材料是否可信，可能不能只看“是不是人写的”，而要看“逻辑是否可验证”。

Lean 4 在这里提供了一个极佳的标准：语言风格可以被 AI 污染，但内核校验的结果不会说谎。只要一份证明能被 Lean 内核完整校验，并且不依赖额外公理，那无论写注释的人是谁，证明本身在数学上就是可信的。换句话说，Claude 文风只是表层的装饰，机器校验的结论才是地基。

所以我觉得，Ethan 那句话与其说是嘲讽，不如说是在提醒读者：接受现实吧，未来会有大量“AI 协作产物”出现在学术和工程领域。我们要学会区分两种审查——一种是审查文风，看它是人写的还是机器写的；另一种是审查逻辑，看它是否经得起验证。前者可能越来越不重要，后者才是需要加强的能力。

5. 常见问题与避坑指南

5.1 形式化证明常见误区

很多初学者拿到 Lean 4，第一反应是“我是不是要把数学全忘掉，改用机器语言思考”。其实不对。Lean 4 的学习曲线陡，但它不要求你放弃数学直觉，反而更依赖你对数学结构的理解。策略只是工具，真正的难点在于识别“这句自然语言证明里，哪些事实是必要的跳步，哪些是可有可无的铺垫”，然后把必要的跳步拆成机器可接受的步骤。

第二个常见误区是过度依赖simp一类的自动化策略。simp确实能做大量化简，但如果你不理解它具体调用了哪些引理，一旦证明卡住，你连调试方向都没有。我见过不少人，在simp后面堆一堆前置条件，结果其中某一条是多余的，导致后面用rw时目标变形，找半天找不到问题。更健康的做法是先弄清目标长什么样，再决定用哪个策略，必要时用trace_state查看当前目标。

第三个误区是把公理和引理混为一谈。Lean 里#print axioms列出的如果不是空表，说明你的证明依赖了额外假设。有些常用策略会引入少量公理，你需要确认它们是否在可接受范围内。对于数论主定理的证明，理想状态下公理列表应该非常简短。

这里整理一个简单速查表：

5.2 关于“AI 文风”的几个现实问题

在讨论 AI 生成内容时常有人问：能不能通过改文风避免被识别？答案是能，但很费劲，取决于你改得多彻底。模型生成的文本，即使经过一轮人工润色，仍可能保留某些连接词频率、段落长度的统计特征。真要彻底消除 AI 指纹，需要逐句改写，成本往往比你自己写一遍还高。

另一个现实问题是：文风识别会不会误伤人类作者？会。我认识一位老师，写作风格非常规整、总分总结构强，几乎每次都被怀疑是 AI。所以不要拿“像不像 AI”当唯一判断标准，尤其对人。判断一份文本是否可信，更应该看事实来源是否清楚、论证是否完整、能否被复现。

对使用 AI 辅助工作的人来说，我的建议是：别试图伪装成“无 AI 参与”。与其把文风识别当敌我识别器，不如在项目里明确标注哪些部分由 AI 生成、哪些由人审阅，这也方便后续维护者了解文档的可信边界。Anthropic 这次的公开做法，虽然被 Ethan 抓出了文风指纹，但整体是透明的，这其实是一个值得推广的示范。

5.3 一些值得现在就试的操作建议

如果你读到这里，对 Lean 4 或 AI 辅助证明产生了兴趣，我的建议是不要从一开始就盯着费马大定理，先从小事做起。

第一步，装好 Lean 4 和 mathlib 环境，跑通一个最简单的example。目标不是“学会 Lean”，而是感受“命题即类型、证明即构造”的基本流程。第二步，挑一个你已经会证的中学或本科定理，比如二次方程的求根公式、二项式展开，用 Lean 4 去正式证明它。这个过程中你会大量遇到“明明人眼知道必然成立，机器却要求你一点一点展开”的挫败感，这种挫败感恰恰是理解形式化验证价值的最好入口。

第三步，熟练之后再尝试引入 AI 辅助：把定理描述和上下文粘贴给 Claude，让它生成候选策略，你负责审查和编译。打开#print axioms检查依赖，单独验证可疑的by块。整个过程看起来慢，但它能帮你形成一种“逻辑可验证”的工作习惯，这种习惯在 AI 生成内容越来越多的今天，可能比掌握哪一个模型本身更值钱。

最后再分享一个小技巧：如果你在 GitHub 上看到别人公开的大型 Lean 证明项目，别只盯着主定理文件，先看它的lean-toolchain、lakefile和依赖结构。这三样东西决定了你能不能复现、复现成本有多高。Anthropic 这份 FLT 项目如果公开完整，按我的经验，单纯把整个依赖树编译一遍就需要不少时间，所以想复现的话，提前规划好机器资源，也留足耐心。

我个人的体会是，这次事件最大的看点就在“Claude 文风”这四个字。当一份以消除人类主观瑕疵为目标的机器校验证明文档，自身也带着 AI 的表达指纹时，我们应该认真接受一个事实：AI 已经浸润到知识生产最核心的环节。而我们能依赖的，不是拒绝 AI，而是建立在可验证逻辑之上的、更强的审查机制。Lean 4 给出了一种审查机制，文风识别给出的是另一种信号，两者结合，才是未来人机协作时代相对稳固的底座。