如果你平时关注形式化验证最近应该被一条消息刷屏了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 4AI 公司参与定理证明的动机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 是一个交互式定理证明器。你给它几个公理、几个定义它通过一套类型系统和归纳构造演算把“命题就是类型证明就是构造该类型的项”这个思想做到极致。你的目标不是写程序而是构造一个满足指定类型也就是命题的证明项。听起来玄乎拿加法举例命题“224”在 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_numnorm_num的作用是直接对数值表达式求值并化简。两条代码走完全不同的路径但最终都会得到同一个结论在 Lean 4 的 kernel 看来证明成立。对新手来说最该理解的一点是“by后面那一长串 tactic 不是给人看的是给内核检查的证据生成脚本”。如果你希望证明更容易人读可以改用calc块example (x y : Nat) : (x y) ^ 2 x^2 2*x*y y^2 : by ringring策略处理半环上的多项式等式。每个策略都封装了一批底层推理规则策略成功后Lean 会把证明项展开交给内核校验。所以所谓“Lean 4 证明”本质上是一棵树叶节点是公理和已知定理内部节点由 tactic 生成根节点是你要证明的命题。树越大证明越庞大。一份费马大定理级别的证明不是几百行而是几十万行、上百万行公式结构和经过精心组织的前置引理。2.3 可校验证明的结构特征Lean 社区把大型证明项目叫“证明开发”。它们一般有几个共同特征模块化大定理被拆成许多小引理每个引理独立可编译编译过后可作为新的引理被后续使用。高度依赖 mathlibmathlib 是 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 -- 这里是某个中间步骤 sorrysorry在 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列出的如果不是空表说明你的证明依赖了额外假设。有些常用策略会引入少量公理你需要确认它们是否在可接受范围内。对于数论主定理的证明理想状态下公理列表应该非常简短。这里整理一个简单速查表现象可能原因建议simp什么都没有化简目标结构不支持或依赖引理未导入先unfold相关定义再用simp编译超时单个策略块处理信息量过大拆分多个have中间结论提交后发现sorry残留开发时占位未清零提交前全局搜索并逐条处理证明通过但不敢信任隐式依赖额外公理运行#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 给出了一种审查机制文风识别给出的是另一种信号两者结合才是未来人机协作时代相对稳固的底座。