数学证明的“AI 指纹”费马大定理的 Lean 4 形式化与 Claude 文风疑云前几天圈子里传了个挺有意思的消息Anthropic 上传了一份基于 Lean 4 的费马大定理机器校验证明结果被 Ethan Mollick 一眼看出文档里带着明显的 Claude 文风。这事儿妙就妙在它把两件看起来八竿子打不着的事捏在了一起——一边是人类数学史上最著名的“我有个绝妙的证明但这里写不下”另一边是大模型写技术文档时那股藏不住的“AI 味”。先说结论这不是什么学术造假现场也不涉及“AI 是否真正证明了定理”这种哲学争论。事实是费马大定理的形式化验证在 Lean 社区早就是一项正在进行中的工程壮举Anthropic 这次的动作更像是把这项工作的部分成果、分析报告或辅助文档用自家模型整理后公开出来。真正引发讨论的点在于当 AI 参与数学写作时它留下的风格痕迹反而成了人类识别它的“指纹”。这篇文章我想从几个角度展开聊聊Lean 4 到底是个什么东西、费马大定理这种级别的问题怎么在计算机里被“校验”、以及从“Claude 文风”这个细节里我们能观察到 AI 参与严肃知识生产的哪些现实状态。不管你是搞形式化验证的、玩大模型的还是单纯对数学和 AI 交叉感兴趣这篇都值得你花十分钟慢慢看。1. 事件全貌一个证明、一个风格、一场讨论1.1 Ethan Mollick 到底发现了什么Ethan Mollick 是沃顿商学院研究 AI 对工作影响的教授他日常干的事就是拿各种 AI 工具做实验然后观察输出质量。这次他看到 Anthropic 上传的 Lean 4 费马大定理相关文档后指出一个非常细的观察点文档里那些“先给一个加粗的总结句然后用冒号引出细节”的写法、那种“值得注意的是”的过渡句式、还有某些段落里刻意均匀的节奏感一眼就是 Claude 家族的文风。这听起来像是个小事但细想其实挺震撼。费马大定理是什么体量是让数学家折腾了三百多年的问题1994 年才被 Andrew Wiles 用极其复杂的椭圆曲线和模形式理论攻克光是证明就有上百页。要把这种级别的证明搬进 Lean 4 里做机器校验工作量是普通人难以想象的。而就是这样一份被公认为“人类数学最高成就之一”的证明文档里居然能被人一眼认出“这是 AI 帮忙写的”。这背后其实暴露了一个当前 AI 辅助科研的真实状态AI 不是在做数学的核心推导它在做的是整理、转述、结构化和润色这些“周边工作”。但即便是周边工作它仍然带着自己鲜明的风格烙印。1.2 为什么这件事值得从业者关注如果你跟我一样平时既接触大模型应用也稍微关注一点形式化方法就会知道这件事真正值得咀嚼的地方有两层。第一层是技术意义上的Lean 4 正在成为数学界验证复杂证明的重要基础设施而费马大定理是这种基础设施能触及的天花板级别的试金石。一旦像费马大定理这种级别的证明被完整形式化说明 Lean 的数学库和验证能力已经成熟到可以支撑真正前沿的数学研究。第二层是社会学意义上的AI 生成内容正在大规模融入学术生产而“作者身份”和“AI 辅助程度”的边界正在变得模糊。一篇文档里“有人类写的部分又有 AI 整理的部分”这在未来会成为常态。Ethan Mollick 的这个观察本质上是在告诉我们AI 参与知识生产的痕迹已经细微到可以从用词习惯里去辨认了。这两个层面叠加在一起才是这条新闻真正有嚼头的地方。2. Lean 4把数学证明变成机器能检查的程序2.1 一个普通程序员眼里的 Lean 4如果你没接触过 Lean可以把它理解成一种同时具备“编程语言”和“证明助手”属性的东西。你在 Lean 里写下的每一段代码本质上都是在构造一个数学证明而 Lean 的内核会一步步检查你的证明是否严格站得住脚。它跟普通的编程语言很像有函数、有类型、有递归定义但它多了一个杀手级能力你可以写出一个命题然后给出这个命题的证明机器会验证你的证明过程在逻辑上是不是无懈可击。这听起来很抽象我给你看一段最简单的 Lean 4 代码你大概就有感觉了-- 定义对于任意自然数 aa 0 a theorem add_zero (a : Nat) : a 0 a : by simp -- 定义加法交换律 theorem add_comm (a b : Nat) : a b b a : by sorry上面这段代码里theorem是用来声明一个定理的冒号后面跟的是要证明的命题: by后面的部分是证明脚本。我第一个定理用了simp这个自动化策略它会把简单的恒等式直接交给机器推理。第二个定理我写了sorry这在 Lean 里是个“作弊”命令意思是“我承认这个定理是对的但我懒得现在证明”实际使用时是严重不推荐的——因为它的存在意味着证明还不完整。真正的 Lean 证明尤其是数学库mathlib里的证明充满了各种策略组合、归纳推理、以及复杂的不动点论证。它读起来更像一门严谨的逻辑语言而不是日常的自然语言数学论文。2.2 为什么数学家需要 Lean 这种“证明编译器”搞数学的人大概都有过这种体验审稿人跟你说“你这步跳得有点大能否补充细节”或者你自己回头读半年前的论文草稿发现有些步骤自己也看得云里雾里。传统的数学证明本质上是一个“人类对人类的交流”它默认读者和作者共享大量背景知识所以很多步骤可以“省略”。Lean 的出现改变了这个格局。它不关心你有没有背景知识它只关心你的推导是否真的每一步都符合逻辑规则。在 Lean 里你能用的每一个推理步骤都被编码成了一组规则任何超出规则的跳跃都会被机器直接拒绝。这就相当于把数学证明从“写作文”变成了“写程序”——你不能只说“显然成立”你得让编译器通过才行。打个比方如果说传统数学证明是用文字描述一条路线图那么 Lean 里的证明就像是拿着 GPS 一步步走完整个路线每一步都要验证自己踩在了真实的地面上而不是说“这里大概有一条路”。数学界之所以越来越重视 Lean是因为当证明的复杂度大到一定程度比如费马大定理人类检查证明的难度已经高到了不可靠的程度。有了 Lean你可以让机器把整条证明链路的每一步都检查一遍理论上可以把“人为疏漏”的可能性几乎降为零。2.3 Lean 4 与 Lean 3 的变化以及它的“门槛”如果你在 2023 年之前关注过 Lean大概率用的是 Lean 3。后来 Lean 社区整体迁移到了 Lean 4这算是一次大版本换代语言本身有了很多改变编译速度更快、宏系统更强、和外部工具的交互也更方便。但从一个使用者的角度来看Lean 4 最大的变化其实是生态的成熟。mathlib这个集合了数千名贡献者工作的数学库在 Lean 4 下已经积累了几百万行代码涵盖了从基础代数、分析、拓扑到数论、代数几何的大量内容。正是因为 mathlib 积累到了一定的丰富程度才让像费马大定理这种级别的形式化工作成为可能。不过说实话Lean 4 的上手门槛相当高。它不是那种“看两小时文档就能写证明”的工具。你需要同时具备三样基础数理逻辑的基本素养、数学证明的直觉以及一定的函数式编程思维。很多人卡在第一步是因为思维切换不过来——从“我想证明什么”到“我该怎么跟机器说清楚”中间的鸿沟比想象中大得多。3. 费马大定理的机器校验一场数学界的“软件工程”3.1 证实与证伪的边界为什么费马大定理适合做形式化费马大定理说的是当 n 大于 2 时方程 x^n y^n z^n 没有正整数解。费马在 1637 年声称自己有一个绝妙的证明但没人找到过。这个定理的“恶名”在于它看起来非常简单——初中生都能理解——但证明起来却牵扯到了二十世纪最深刻的数学工具。Andrew Wiles 在 1994 年完成的证明核心路线是如果存在反例就可以构造出一个半稳定的椭圆曲线称为 Frey 曲线然后通过谷山-志村猜想后成为定理得出该曲线对应一个模形式再结合 Ribet 定理证明这种模形式不可能存在从而引出矛盾。这条证明路线里的每一步都是硬骨头每一步都依赖大量前置定理。当人类数学家审阅 Wiles 的证明时早期版本确实还出过一次漏洞后来花了很大功夫才补上。这件事让很多人开始反思如果连 Wiles 这种级别的数学家都会在一份长达一百多页的证明里留下漏洞那么对于更复杂的数学证明传统审稿模式是不是已经很不可靠了这正是形式化验证登场的时候。与其让几个审稿人吃力地核对每一步不如让机器把整条逻辑链推一遍。费马大定理因此在 Lean 社区被视为一个终极测试项目——如果你能在 Lean 里完成 Fermat 大定理的形式化就说明这个系统已经成熟到足以支撑人类最前沿的数学。3.2 项目规模这不是一个人的工作现在简单说说这个项目到底有多大。Lean 数学库mathlib为了支撑费马大定理的证明需要提供大量前置数学基础设施包括但不限于椭圆曲线的基本理论模形式与 Hecke 代数岩泽理论的若干关键结论Galois 表示论Ribet 定理的完整形式化这些内容在 Lean 里被拆分成了数以千计的定理文件整个关联的代码文件规模以几十万行计算。单个文件的证明可能只有几行但为了这几行背后要搭起一整套数学体系。这非常像大型软件工程——你为了一个核心函数需要搭建整个底层框架。实际上费马大定理在 Lean 中的完整形式化是一个长期推进的社区项目。2021 年就有研究者宣布完成了 FLTFermats Last Theorem的形式化工作用到了 Ribet 定理和谷山-志村定理。当时这个新闻在数学圈和编程圈都引起了不小的轰动。而这次 Anthropic 上传的东西从标题到内容显然是在这个方向上继续推进——或者说把已有的形式化工作用更系统的方式整理、呈现出来。3.3 机器校验证明的“含金量”到底有多高有些人可能会误解以为 Lean 校验过证明之后就“万事大吉”了。这里必须说清楚Lean 校验的严谨性是有条件的它依赖于三件事——一是你引用的前置定理是否被正确形式化二是你对原证明的解读是否准确三是 mathlib 底层的逻辑公理体系本身没有矛盾。换句话说如果你在前置定理的形式化过程中犯了错那么后面所有依赖它的证明都会跟着错。这也是 Lean 社区非常强调“从公理出发逐步建立”的原因。mathlib 里每个定理都必须可以回溯到更基础的定理最终回溯到 Lean 内核里的少数公理。这种从基础到高层的严格树状结构保证了只要底层不出问题上层就不会出问题。所以你可以把 Lean 的证明校验理解成一条逻辑链它不负责“告诉你怎么证明”它只负责“检查你的证明是否每一步都合规”。而这种检查的强度和精度是人类审稿完全做不到的。也正因为如此费马大定理一旦在 Lean 里被完整验证其意义不亚于当年 Wiles 的原始证明——它把“这个证明是对的”从“极大概率是对的”提升到了“机器可以逐行确认”的程度。4. “Claude 文风”背后AI 写作的指纹与残余4.1 如何识别一段文字是 AI 写的说回 Ethan Mollick 那个观察。他提到的“Claude 文风”其实指向一组非常具体、可操作的语言特征。我自己长期跟 Claude 系列模型打交道总结下来 AI 生成的学术文本通常有这几个明显特征开头喜欢加粗总结句。比如“费马大定理是数论中最重要的定理之一。该定理指出……”这种写法在人类论文里很少见但 Claude 生成时非常偏好这种“先给结论再展开”的结构。连接词过于规矩。“值得注意的是”“不难看出”“综上所述”“由此可见”这些套话出现的频率远超正常人类写作者。段落节奏均匀到不真实。AI 生成的段落长度往往高度一致每段三到五句每句的信息密度差异不大读起来缺少人类写作那种“呼吸感”和“偏重感”。让步从句使用频繁。“虽然……但是……然而……”这类转折结构在 AI 文本里出现得异常密集因为它需要显得“客观中立”。列表和冒号的仪式感。AI 特别喜欢用冒号引出内容把原本适合揉进叙述里的细节强行拆成条目化展示。如果你回头去看自己手头的文档但凡有这些特征的十有八九是 AI 参与过。Ethan Mollick 这次只是把这种直觉推广到了一个极端严肃的数学文档上——结果同样成立可见 AI 的风格烙印真的很深。4.2 为什么“AI 味”去不掉模型的语言先验你得理解一件事Claude 之所以有“Claude 文风”不是因为它被训练成那个样子而是它所依赖的预训练目标决定了它必然偏好“高概率的、规整的、常见的”语言表达方式。在一个大规模语料里像“值得注意的是”这种过渡短语出现的频率远高于一个人类作者的自然表达频率所以模型在生成文本时会优先选择这些“高概率路径”。换句话说AI 不是故意要写得像 AI而是它的自然状态就是“过度平滑”。你让它自由发挥它最后输出的文本就会朝着语料里最常见、最典型的表达方式回归。这就像你让一个从没见过现代时尚的古代人写“关于服装风格的调查报告”他一定会努力把每种服装类型的特征都写得很规整、很平均因为他没有“个人品味”和“下意识偏好”可言。想要真正去掉 AI 味唯一可行的办法是给模型注入足够强的风格约束——比如明确指定“不要用加粗开头”“不要用值得注意的是”“每段不超过三句”——或者用人类作者大规模润色。但完全看不出痕迹的难度非常高总会在某个角落留下一个“安全、通用、平滑”的用词习惯。4.3 “文档带 AI 味”这件事本身是坏消息吗我猜很多人看到 Ethan Mollick 那个发现之后第一反应是“哎AI 辅助科研是不是还是不够成熟”。但我不这么看。注意这件事的重点是“文档带有 Claude 文风”而不是“证明本身有逻辑错误”。这恰恰说明 AI 在参与这个项目的过程中承担的角色是写作和整理而证明的核心逻辑和验证流程始终掌握在人和机器内核手里。换个角度想如果一份费马大定理的整理文档用 AI 来写能写得清晰、结构完整同时还能被其他数学家检索和阅读这不是“降级”这是“提效”。真正值得警惕的不是 AI 写了文档而是文档的“作者署名”不透明。如果 AI 参与了生成但不在任何地方声明那才是学术伦理问题。Anthropic 这次是自己上传自己的项目模型是他们自家的文档风格是自家产品的特征自然也没什么可遮遮掩掩的——这反而让我们有了一个观察窗口当 AI 成为科研写作的参与者它留下的“指纹”其实是帮助我们识别 AI 参与程度的一个有效信号。4.4 Claude Code 时代的写作与验证一点延伸思考现在热词里关于 Claude Code 的讨论非常多很多人已经在用 AI 编写代码、写测试、生成技术文档。从我的使用体验来看Claude Code 这类工具在“辅助实现”上的价值已经非常明确我让它帮我生成一个 Lean 4 证明的初稿它可以迅速把结构和主要步骤搭出来我再手动审核和完善细节省掉了很多从零开始的精力。但随之而来的问题是当你用 Claude Code 这类工具辅助一个严肃的工程或数学证明时你必须负起“最终审核”的责任。机器生成的内容再流畅也不能替代你对核心逻辑的把关。拿 Lean 4 来说你可以让 Claude 帮你写证明脚本的框架但最终sorry要不要去掉、证明步骤是否严谨仍然需要你逐行检查。工具负责的是降低起步门槛负责不了“证明正确”这件事。Ethanol Mollick 的观察在这一点上其实给了我们一个很好的提醒无论 AI 的参与程度多深最终发布的内容都应该有清晰的责任人和审核痕迹。文档里有“AI 味”不可怕可怕的是没人承认、没人检查、没人对结果负责。5. 如果你想体验 Lean 4实操入门与避坑心得既然聊到了 Lean 4我猜很多人会想“要不我也试试看”。这里我给你一份不啰嗦的入门路径包括环境的搭建、基本操作的常用命令以及我踩过几次坑之后总结出来的心得。直接照着走就行。5.1 本地环境搭建VS Code 插件方案要用 Lean 4最常规的选择是 VS Code 加官方插件。步骤就三步安装 VS Code这步不用展开装完就行。在扩展市场里搜lean4安装由 Lean 社区维护的官方扩展。用elan安装 Lean 4 工具链管理器。elan是 Lean 的版本管理器功能类似于 Node 生态里的nvm。装好之后你只需要在终端里执行curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh然后创建一个目录放你的第一个项目在里面放一个名为lakefile.lean的文件内容可以简单写import Mathlib这行的意思是引入整个 mathlib 数学库。第一次跑的时候加载会有点慢因为 mathlib 编译和缓存需要时间。如果你的机器性能一般这一步会特别考验耐心。5.2 写第一个定理从 AddComm 开刀环境准备好之后建议先不要直接挑战费马大定理——那个级别不是你第一天能碰的。从最基础的定理开始先理解“证明脚本”是怎么工作的。新建Test.lean输入以下内容import Mathlib theorem my_add_comm (a b : Nat) : a b b a : by exact Nat.add_comm a b把光标放到exact那一行VS Code 右侧的信息面板会显示证明状态。当你看到No goals时就说明证明通过了。这里有个小技巧在写证明之前可以先输入by然后按回车让 Lean 告诉你当前需要证明什么。很多时候你只是不知道自己该往哪个方向走Lean 的信息面板会帮你理清头绪。我最初学 Lean 的时候最常做的事就是“空着证明让工具告诉我该证明什么”这种方式比硬背代码有效得多。5.3 一个好用到离谱的辅助命令apply?证明写不出来怎么办我常用一个叫apply?的命令它可以搜索 mathlib 里已有的定理看哪些能用于当前目标。举个例子theorem test (a b : Nat) : a b b a : by apply?把光标放在apply?那行Lean 会在当前证明目标下搜索可用的定理然后把建议列出来。相当于是“帮你查手册”。配合exact、rw、simp、omega这几个核心策略大部分入门证明都能搞定。omega是专门解线性和自然数算术等式的用起来非常省心。5.4 踩坑记录与避坑技巧我学 Lean 的过程中踩过不少坑挑几个有用的分享给你坑一直接啃官方文档容易劝退。官方文档质量很高但它的读者对象不是零基础用户。我建议先看社区里现成的教程视频或入门文章配合动手操作建立感觉再回头翻官方文档查细节效率高得多。坑二跟 Lean 3 的旧教程学然后全学废了。网上很多早期教程是基于 Lean 3 的语法跟 Lean 4 有差异。拿到一个教程先确认它是不是 Lean 4 版本不然你抄进去的代码大概率编译不过。坑三编译太慢心态爆炸。第一次 import Mathlib 后编译可能要很久这是正常的。解决方法是设置 Lake 的缓存把编译结果存好第二次就不用重新编了。具体操作是在项目目录执行lake exe cache get这会从远程缓存拉取预编译的 mathlib 内容省掉本地重新编译的痛苦。如果你遇到网络问题导致拉取失败也别死磕多试几次或者换个网络环境往往就解决了。坑四把sorry留在代码里。写证明的时候经常想“这个我先 sorry 一下回头再证”结果回头就忘了。一旦代码里有sorryLean 不会报错会直接当作“这个证明已通过”。这是很大的隐患——以后你引用这个定理它会污染整条证明链。建议养成习惯提交前全局搜索sorry清一遍。5.5 当 Lean 4 遇到 Claude一个实际的工作流最后分享一下我现在的工作流。当我需要写一个比较复杂的 Lean 4 证明时我不会手动从头写而是先在纸上理清证明思路然后把思路用自然语言描述给 Claude让它生成一个符合 Lean 4 语法的证明脚本初稿。注意Claude 生成的代码经常有一个问题它会把一些高级策略用得很花哨但有时会引用一个其实不存在的定理名或者逻辑上偷工减料。所以拿到初稿后我不会直接信任而是逐行放回 Lean 环境里跑用信息面板检查每一行是否真的通过了。这套流程下来效率大概比纯手写高出四五成但同时付出的是“审查成本”——你必须足够熟悉 Lean 语法才能分辨 Claude 给的代码哪里是对的、哪里是在糊弄。说到底AI 辅助工具是放大器不是替代品。你原本的水平决定了工具放大后的结果。这个体验其实恰好回到标题里 Ethan Mollick 那个观察AI 生成的内容自带风格和潜在风险关键是“有没有人在最终环节把关”。在 Lean 的世界里把关者是人和逻辑内核在文档世界里把关者同样得是负责任的作者。费马大定理的形式化验证和“Claude 文风”的识别看似是两个话题实际上指向的是同一个问题当 AI 越来越深地嵌入知识生产我们该怎么确定什么是对的、谁对什么负责。Lean 给了一个很好的答案——机器校验与人工审核共同把关Ethan Mollick 的观察则提醒我们即便不在形式化的世界里“这到底是谁写的”也仍然是一个值得追问的好问题。我自己在这段时间里的体会是与其纠结 AI 有没有“数学能力”不如把它当作一个极其擅长起草、整理和复述的强大劳动力。真正决定一份工作价值的始终是你能不能在它给出的东西之上做出正确的判断和取舍。这一点在费马大定理的证明项目里成立在日常用 Claude 辅助工作的场景里也同样成立。
当Lean 4遇见费马大定理：AI数学证明的风格指纹
数学证明的“AI 指纹”费马大定理的 Lean 4 形式化与 Claude 文风疑云前几天圈子里传了个挺有意思的消息Anthropic 上传了一份基于 Lean 4 的费马大定理机器校验证明结果被 Ethan Mollick 一眼看出文档里带着明显的 Claude 文风。这事儿妙就妙在它把两件看起来八竿子打不着的事捏在了一起——一边是人类数学史上最著名的“我有个绝妙的证明但这里写不下”另一边是大模型写技术文档时那股藏不住的“AI 味”。先说结论这不是什么学术造假现场也不涉及“AI 是否真正证明了定理”这种哲学争论。事实是费马大定理的形式化验证在 Lean 社区早就是一项正在进行中的工程壮举Anthropic 这次的动作更像是把这项工作的部分成果、分析报告或辅助文档用自家模型整理后公开出来。真正引发讨论的点在于当 AI 参与数学写作时它留下的风格痕迹反而成了人类识别它的“指纹”。这篇文章我想从几个角度展开聊聊Lean 4 到底是个什么东西、费马大定理这种级别的问题怎么在计算机里被“校验”、以及从“Claude 文风”这个细节里我们能观察到 AI 参与严肃知识生产的哪些现实状态。不管你是搞形式化验证的、玩大模型的还是单纯对数学和 AI 交叉感兴趣这篇都值得你花十分钟慢慢看。1. 事件全貌一个证明、一个风格、一场讨论1.1 Ethan Mollick 到底发现了什么Ethan Mollick 是沃顿商学院研究 AI 对工作影响的教授他日常干的事就是拿各种 AI 工具做实验然后观察输出质量。这次他看到 Anthropic 上传的 Lean 4 费马大定理相关文档后指出一个非常细的观察点文档里那些“先给一个加粗的总结句然后用冒号引出细节”的写法、那种“值得注意的是”的过渡句式、还有某些段落里刻意均匀的节奏感一眼就是 Claude 家族的文风。这听起来像是个小事但细想其实挺震撼。费马大定理是什么体量是让数学家折腾了三百多年的问题1994 年才被 Andrew Wiles 用极其复杂的椭圆曲线和模形式理论攻克光是证明就有上百页。要把这种级别的证明搬进 Lean 4 里做机器校验工作量是普通人难以想象的。而就是这样一份被公认为“人类数学最高成就之一”的证明文档里居然能被人一眼认出“这是 AI 帮忙写的”。这背后其实暴露了一个当前 AI 辅助科研的真实状态AI 不是在做数学的核心推导它在做的是整理、转述、结构化和润色这些“周边工作”。但即便是周边工作它仍然带着自己鲜明的风格烙印。1.2 为什么这件事值得从业者关注如果你跟我一样平时既接触大模型应用也稍微关注一点形式化方法就会知道这件事真正值得咀嚼的地方有两层。第一层是技术意义上的Lean 4 正在成为数学界验证复杂证明的重要基础设施而费马大定理是这种基础设施能触及的天花板级别的试金石。一旦像费马大定理这种级别的证明被完整形式化说明 Lean 的数学库和验证能力已经成熟到可以支撑真正前沿的数学研究。第二层是社会学意义上的AI 生成内容正在大规模融入学术生产而“作者身份”和“AI 辅助程度”的边界正在变得模糊。一篇文档里“有人类写的部分又有 AI 整理的部分”这在未来会成为常态。Ethan Mollick 的这个观察本质上是在告诉我们AI 参与知识生产的痕迹已经细微到可以从用词习惯里去辨认了。这两个层面叠加在一起才是这条新闻真正有嚼头的地方。2. Lean 4把数学证明变成机器能检查的程序2.1 一个普通程序员眼里的 Lean 4如果你没接触过 Lean可以把它理解成一种同时具备“编程语言”和“证明助手”属性的东西。你在 Lean 里写下的每一段代码本质上都是在构造一个数学证明而 Lean 的内核会一步步检查你的证明是否严格站得住脚。它跟普通的编程语言很像有函数、有类型、有递归定义但它多了一个杀手级能力你可以写出一个命题然后给出这个命题的证明机器会验证你的证明过程在逻辑上是不是无懈可击。这听起来很抽象我给你看一段最简单的 Lean 4 代码你大概就有感觉了-- 定义对于任意自然数 aa 0 a theorem add_zero (a : Nat) : a 0 a : by simp -- 定义加法交换律 theorem add_comm (a b : Nat) : a b b a : by sorry上面这段代码里theorem是用来声明一个定理的冒号后面跟的是要证明的命题: by后面的部分是证明脚本。我第一个定理用了simp这个自动化策略它会把简单的恒等式直接交给机器推理。第二个定理我写了sorry这在 Lean 里是个“作弊”命令意思是“我承认这个定理是对的但我懒得现在证明”实际使用时是严重不推荐的——因为它的存在意味着证明还不完整。真正的 Lean 证明尤其是数学库mathlib里的证明充满了各种策略组合、归纳推理、以及复杂的不动点论证。它读起来更像一门严谨的逻辑语言而不是日常的自然语言数学论文。2.2 为什么数学家需要 Lean 这种“证明编译器”搞数学的人大概都有过这种体验审稿人跟你说“你这步跳得有点大能否补充细节”或者你自己回头读半年前的论文草稿发现有些步骤自己也看得云里雾里。传统的数学证明本质上是一个“人类对人类的交流”它默认读者和作者共享大量背景知识所以很多步骤可以“省略”。Lean 的出现改变了这个格局。它不关心你有没有背景知识它只关心你的推导是否真的每一步都符合逻辑规则。在 Lean 里你能用的每一个推理步骤都被编码成了一组规则任何超出规则的跳跃都会被机器直接拒绝。这就相当于把数学证明从“写作文”变成了“写程序”——你不能只说“显然成立”你得让编译器通过才行。打个比方如果说传统数学证明是用文字描述一条路线图那么 Lean 里的证明就像是拿着 GPS 一步步走完整个路线每一步都要验证自己踩在了真实的地面上而不是说“这里大概有一条路”。数学界之所以越来越重视 Lean是因为当证明的复杂度大到一定程度比如费马大定理人类检查证明的难度已经高到了不可靠的程度。有了 Lean你可以让机器把整条证明链路的每一步都检查一遍理论上可以把“人为疏漏”的可能性几乎降为零。2.3 Lean 4 与 Lean 3 的变化以及它的“门槛”如果你在 2023 年之前关注过 Lean大概率用的是 Lean 3。后来 Lean 社区整体迁移到了 Lean 4这算是一次大版本换代语言本身有了很多改变编译速度更快、宏系统更强、和外部工具的交互也更方便。但从一个使用者的角度来看Lean 4 最大的变化其实是生态的成熟。mathlib这个集合了数千名贡献者工作的数学库在 Lean 4 下已经积累了几百万行代码涵盖了从基础代数、分析、拓扑到数论、代数几何的大量内容。正是因为 mathlib 积累到了一定的丰富程度才让像费马大定理这种级别的形式化工作成为可能。不过说实话Lean 4 的上手门槛相当高。它不是那种“看两小时文档就能写证明”的工具。你需要同时具备三样基础数理逻辑的基本素养、数学证明的直觉以及一定的函数式编程思维。很多人卡在第一步是因为思维切换不过来——从“我想证明什么”到“我该怎么跟机器说清楚”中间的鸿沟比想象中大得多。3. 费马大定理的机器校验一场数学界的“软件工程”3.1 证实与证伪的边界为什么费马大定理适合做形式化费马大定理说的是当 n 大于 2 时方程 x^n y^n z^n 没有正整数解。费马在 1637 年声称自己有一个绝妙的证明但没人找到过。这个定理的“恶名”在于它看起来非常简单——初中生都能理解——但证明起来却牵扯到了二十世纪最深刻的数学工具。Andrew Wiles 在 1994 年完成的证明核心路线是如果存在反例就可以构造出一个半稳定的椭圆曲线称为 Frey 曲线然后通过谷山-志村猜想后成为定理得出该曲线对应一个模形式再结合 Ribet 定理证明这种模形式不可能存在从而引出矛盾。这条证明路线里的每一步都是硬骨头每一步都依赖大量前置定理。当人类数学家审阅 Wiles 的证明时早期版本确实还出过一次漏洞后来花了很大功夫才补上。这件事让很多人开始反思如果连 Wiles 这种级别的数学家都会在一份长达一百多页的证明里留下漏洞那么对于更复杂的数学证明传统审稿模式是不是已经很不可靠了这正是形式化验证登场的时候。与其让几个审稿人吃力地核对每一步不如让机器把整条逻辑链推一遍。费马大定理因此在 Lean 社区被视为一个终极测试项目——如果你能在 Lean 里完成 Fermat 大定理的形式化就说明这个系统已经成熟到足以支撑人类最前沿的数学。3.2 项目规模这不是一个人的工作现在简单说说这个项目到底有多大。Lean 数学库mathlib为了支撑费马大定理的证明需要提供大量前置数学基础设施包括但不限于椭圆曲线的基本理论模形式与 Hecke 代数岩泽理论的若干关键结论Galois 表示论Ribet 定理的完整形式化这些内容在 Lean 里被拆分成了数以千计的定理文件整个关联的代码文件规模以几十万行计算。单个文件的证明可能只有几行但为了这几行背后要搭起一整套数学体系。这非常像大型软件工程——你为了一个核心函数需要搭建整个底层框架。实际上费马大定理在 Lean 中的完整形式化是一个长期推进的社区项目。2021 年就有研究者宣布完成了 FLTFermats Last Theorem的形式化工作用到了 Ribet 定理和谷山-志村定理。当时这个新闻在数学圈和编程圈都引起了不小的轰动。而这次 Anthropic 上传的东西从标题到内容显然是在这个方向上继续推进——或者说把已有的形式化工作用更系统的方式整理、呈现出来。3.3 机器校验证明的“含金量”到底有多高有些人可能会误解以为 Lean 校验过证明之后就“万事大吉”了。这里必须说清楚Lean 校验的严谨性是有条件的它依赖于三件事——一是你引用的前置定理是否被正确形式化二是你对原证明的解读是否准确三是 mathlib 底层的逻辑公理体系本身没有矛盾。换句话说如果你在前置定理的形式化过程中犯了错那么后面所有依赖它的证明都会跟着错。这也是 Lean 社区非常强调“从公理出发逐步建立”的原因。mathlib 里每个定理都必须可以回溯到更基础的定理最终回溯到 Lean 内核里的少数公理。这种从基础到高层的严格树状结构保证了只要底层不出问题上层就不会出问题。所以你可以把 Lean 的证明校验理解成一条逻辑链它不负责“告诉你怎么证明”它只负责“检查你的证明是否每一步都合规”。而这种检查的强度和精度是人类审稿完全做不到的。也正因为如此费马大定理一旦在 Lean 里被完整验证其意义不亚于当年 Wiles 的原始证明——它把“这个证明是对的”从“极大概率是对的”提升到了“机器可以逐行确认”的程度。4. “Claude 文风”背后AI 写作的指纹与残余4.1 如何识别一段文字是 AI 写的说回 Ethan Mollick 那个观察。他提到的“Claude 文风”其实指向一组非常具体、可操作的语言特征。我自己长期跟 Claude 系列模型打交道总结下来 AI 生成的学术文本通常有这几个明显特征开头喜欢加粗总结句。比如“费马大定理是数论中最重要的定理之一。该定理指出……”这种写法在人类论文里很少见但 Claude 生成时非常偏好这种“先给结论再展开”的结构。连接词过于规矩。“值得注意的是”“不难看出”“综上所述”“由此可见”这些套话出现的频率远超正常人类写作者。段落节奏均匀到不真实。AI 生成的段落长度往往高度一致每段三到五句每句的信息密度差异不大读起来缺少人类写作那种“呼吸感”和“偏重感”。让步从句使用频繁。“虽然……但是……然而……”这类转折结构在 AI 文本里出现得异常密集因为它需要显得“客观中立”。列表和冒号的仪式感。AI 特别喜欢用冒号引出内容把原本适合揉进叙述里的细节强行拆成条目化展示。如果你回头去看自己手头的文档但凡有这些特征的十有八九是 AI 参与过。Ethan Mollick 这次只是把这种直觉推广到了一个极端严肃的数学文档上——结果同样成立可见 AI 的风格烙印真的很深。4.2 为什么“AI 味”去不掉模型的语言先验你得理解一件事Claude 之所以有“Claude 文风”不是因为它被训练成那个样子而是它所依赖的预训练目标决定了它必然偏好“高概率的、规整的、常见的”语言表达方式。在一个大规模语料里像“值得注意的是”这种过渡短语出现的频率远高于一个人类作者的自然表达频率所以模型在生成文本时会优先选择这些“高概率路径”。换句话说AI 不是故意要写得像 AI而是它的自然状态就是“过度平滑”。你让它自由发挥它最后输出的文本就会朝着语料里最常见、最典型的表达方式回归。这就像你让一个从没见过现代时尚的古代人写“关于服装风格的调查报告”他一定会努力把每种服装类型的特征都写得很规整、很平均因为他没有“个人品味”和“下意识偏好”可言。想要真正去掉 AI 味唯一可行的办法是给模型注入足够强的风格约束——比如明确指定“不要用加粗开头”“不要用值得注意的是”“每段不超过三句”——或者用人类作者大规模润色。但完全看不出痕迹的难度非常高总会在某个角落留下一个“安全、通用、平滑”的用词习惯。4.3 “文档带 AI 味”这件事本身是坏消息吗我猜很多人看到 Ethan Mollick 那个发现之后第一反应是“哎AI 辅助科研是不是还是不够成熟”。但我不这么看。注意这件事的重点是“文档带有 Claude 文风”而不是“证明本身有逻辑错误”。这恰恰说明 AI 在参与这个项目的过程中承担的角色是写作和整理而证明的核心逻辑和验证流程始终掌握在人和机器内核手里。换个角度想如果一份费马大定理的整理文档用 AI 来写能写得清晰、结构完整同时还能被其他数学家检索和阅读这不是“降级”这是“提效”。真正值得警惕的不是 AI 写了文档而是文档的“作者署名”不透明。如果 AI 参与了生成但不在任何地方声明那才是学术伦理问题。Anthropic 这次是自己上传自己的项目模型是他们自家的文档风格是自家产品的特征自然也没什么可遮遮掩掩的——这反而让我们有了一个观察窗口当 AI 成为科研写作的参与者它留下的“指纹”其实是帮助我们识别 AI 参与程度的一个有效信号。4.4 Claude Code 时代的写作与验证一点延伸思考现在热词里关于 Claude Code 的讨论非常多很多人已经在用 AI 编写代码、写测试、生成技术文档。从我的使用体验来看Claude Code 这类工具在“辅助实现”上的价值已经非常明确我让它帮我生成一个 Lean 4 证明的初稿它可以迅速把结构和主要步骤搭出来我再手动审核和完善细节省掉了很多从零开始的精力。但随之而来的问题是当你用 Claude Code 这类工具辅助一个严肃的工程或数学证明时你必须负起“最终审核”的责任。机器生成的内容再流畅也不能替代你对核心逻辑的把关。拿 Lean 4 来说你可以让 Claude 帮你写证明脚本的框架但最终sorry要不要去掉、证明步骤是否严谨仍然需要你逐行检查。工具负责的是降低起步门槛负责不了“证明正确”这件事。Ethanol Mollick 的观察在这一点上其实给了我们一个很好的提醒无论 AI 的参与程度多深最终发布的内容都应该有清晰的责任人和审核痕迹。文档里有“AI 味”不可怕可怕的是没人承认、没人检查、没人对结果负责。5. 如果你想体验 Lean 4实操入门与避坑心得既然聊到了 Lean 4我猜很多人会想“要不我也试试看”。这里我给你一份不啰嗦的入门路径包括环境的搭建、基本操作的常用命令以及我踩过几次坑之后总结出来的心得。直接照着走就行。5.1 本地环境搭建VS Code 插件方案要用 Lean 4最常规的选择是 VS Code 加官方插件。步骤就三步安装 VS Code这步不用展开装完就行。在扩展市场里搜lean4安装由 Lean 社区维护的官方扩展。用elan安装 Lean 4 工具链管理器。elan是 Lean 的版本管理器功能类似于 Node 生态里的nvm。装好之后你只需要在终端里执行curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh然后创建一个目录放你的第一个项目在里面放一个名为lakefile.lean的文件内容可以简单写import Mathlib这行的意思是引入整个 mathlib 数学库。第一次跑的时候加载会有点慢因为 mathlib 编译和缓存需要时间。如果你的机器性能一般这一步会特别考验耐心。5.2 写第一个定理从 AddComm 开刀环境准备好之后建议先不要直接挑战费马大定理——那个级别不是你第一天能碰的。从最基础的定理开始先理解“证明脚本”是怎么工作的。新建Test.lean输入以下内容import Mathlib theorem my_add_comm (a b : Nat) : a b b a : by exact Nat.add_comm a b把光标放到exact那一行VS Code 右侧的信息面板会显示证明状态。当你看到No goals时就说明证明通过了。这里有个小技巧在写证明之前可以先输入by然后按回车让 Lean 告诉你当前需要证明什么。很多时候你只是不知道自己该往哪个方向走Lean 的信息面板会帮你理清头绪。我最初学 Lean 的时候最常做的事就是“空着证明让工具告诉我该证明什么”这种方式比硬背代码有效得多。5.3 一个好用到离谱的辅助命令apply?证明写不出来怎么办我常用一个叫apply?的命令它可以搜索 mathlib 里已有的定理看哪些能用于当前目标。举个例子theorem test (a b : Nat) : a b b a : by apply?把光标放在apply?那行Lean 会在当前证明目标下搜索可用的定理然后把建议列出来。相当于是“帮你查手册”。配合exact、rw、simp、omega这几个核心策略大部分入门证明都能搞定。omega是专门解线性和自然数算术等式的用起来非常省心。5.4 踩坑记录与避坑技巧我学 Lean 的过程中踩过不少坑挑几个有用的分享给你坑一直接啃官方文档容易劝退。官方文档质量很高但它的读者对象不是零基础用户。我建议先看社区里现成的教程视频或入门文章配合动手操作建立感觉再回头翻官方文档查细节效率高得多。坑二跟 Lean 3 的旧教程学然后全学废了。网上很多早期教程是基于 Lean 3 的语法跟 Lean 4 有差异。拿到一个教程先确认它是不是 Lean 4 版本不然你抄进去的代码大概率编译不过。坑三编译太慢心态爆炸。第一次 import Mathlib 后编译可能要很久这是正常的。解决方法是设置 Lake 的缓存把编译结果存好第二次就不用重新编了。具体操作是在项目目录执行lake exe cache get这会从远程缓存拉取预编译的 mathlib 内容省掉本地重新编译的痛苦。如果你遇到网络问题导致拉取失败也别死磕多试几次或者换个网络环境往往就解决了。坑四把sorry留在代码里。写证明的时候经常想“这个我先 sorry 一下回头再证”结果回头就忘了。一旦代码里有sorryLean 不会报错会直接当作“这个证明已通过”。这是很大的隐患——以后你引用这个定理它会污染整条证明链。建议养成习惯提交前全局搜索sorry清一遍。5.5 当 Lean 4 遇到 Claude一个实际的工作流最后分享一下我现在的工作流。当我需要写一个比较复杂的 Lean 4 证明时我不会手动从头写而是先在纸上理清证明思路然后把思路用自然语言描述给 Claude让它生成一个符合 Lean 4 语法的证明脚本初稿。注意Claude 生成的代码经常有一个问题它会把一些高级策略用得很花哨但有时会引用一个其实不存在的定理名或者逻辑上偷工减料。所以拿到初稿后我不会直接信任而是逐行放回 Lean 环境里跑用信息面板检查每一行是否真的通过了。这套流程下来效率大概比纯手写高出四五成但同时付出的是“审查成本”——你必须足够熟悉 Lean 语法才能分辨 Claude 给的代码哪里是对的、哪里是在糊弄。说到底AI 辅助工具是放大器不是替代品。你原本的水平决定了工具放大后的结果。这个体验其实恰好回到标题里 Ethan Mollick 那个观察AI 生成的内容自带风格和潜在风险关键是“有没有人在最终环节把关”。在 Lean 的世界里把关者是人和逻辑内核在文档世界里把关者同样得是负责任的作者。费马大定理的形式化验证和“Claude 文风”的识别看似是两个话题实际上指向的是同一个问题当 AI 越来越深地嵌入知识生产我们该怎么确定什么是对的、谁对什么负责。Lean 给了一个很好的答案——机器校验与人工审核共同把关Ethan Mollick 的观察则提醒我们即便不在形式化的世界里“这到底是谁写的”也仍然是一个值得追问的好问题。我自己在这段时间里的体会是与其纠结 AI 有没有“数学能力”不如把它当作一个极其擅长起草、整理和复述的强大劳动力。真正决定一份工作价值的始终是你能不能在它给出的东西之上做出正确的判断和取舍。这一点在费马大定理的证明项目里成立在日常用 Claude 辅助工作的场景里也同样成立。