★ FEATURED ARTICLE 1. 这条热搜到底在说什么先厘清证明费马大定理的真实含义先把最容易误解的一点讲清楚所谓Claude AI 快速证明了费马大定理在绝大多数实际语境里指的并不是AI独立给出了一个全新的、被数学界认可的完整证明而是借助AI把一个已经被人类证明过的定理用Lean这种形式化证明语言重新写了一遍并且在这个过程中大幅压缩了人工耗时。这两件事的差别非常大前者是数学发现后者是形式化工程。热搜标题为了传播效果把两者混为一谈但作为从业者我们必须把边界划清楚否则后面所有的技术讨论都会跑偏。费马大定理本身在1994年就由Andrew Wiles给出了完整证明这是公认的数学史事件。而Lean是一个交互式定理证明器interactive theorem prover它要求你把每一步推理都写成机器能检查的形式任何跳步、任何显然成立都不被接受。所以用Lean证明费马大定理这件事本质上是把人类已有的数学证明翻译成一套严格的、可被机器逐行验证的代码。这个翻译过程极其枯燥历史上需要大量人力而AI的价值恰恰在于加速这个翻译和补全的过程。那为什么这件事值得关注因为形式化证明是当前AI能力的一个硬考场。它不像写文章、写代码那样可以含糊其辞每一步都必须逻辑自洽机器会毫不留情地报错。一个AI能不能在Lean里把证明推进下去直接反映了它在长链条推理、上下文保持、错误自我修正上的真实水平。这也是为什么关键词里同时出现了Claude AI、Lean、编程语言、GitHub、Token这些词——它们共同指向一个完整的技术链路用AI辅助在Lean里完成形式化证明代码托管在GitHub上整个过程消耗大量Token。需要说明的是下面涉及的具体操作步骤、参数配置、工具选型都是基于当前形式化证明和AI辅助编程的常见实践做的合理补全因为原始输入里并没有给出细节。我会明确标注哪些是通用做法哪些是我个人经验里的取舍。2. Lean为什么成了AI推理能力的试金石2.1 Lean和普通编程语言的本质区别大多数人熟悉的编程语言比如Python、JavaScript是告诉计算机怎么做你写的是指令运行结果是数据。Lean完全是另一回事你写的是命题和证明运行结果是这个证明是否成立。在Lean里一个定理的证明过程会被编译成一个叫做term的东西然后由内核kernel逐条检查类型是否正确。只要有一处不成立整个证明就编译不过。这就带来一个关键特性Lean不会骗你也不会被你骗。你没法像写业务代码那样用try-catch把错误吞掉也没法写个TODO先糊弄过去。证明要么完整要么不存在。这种全有或全无的性质让它成为检验AI推理能力的理想场景——AI没法靠语言上的流畅蒙混过关。Lean的数学库叫Mathlib是目前最大的形式化数学库之一里面已经沉淀了大量定理和引理。用Lean做证明很多时候不是从零开始而是在Mathlib里找到合适的引理然后把它拼装起来。这个找引理的过程恰恰是AI比较擅长的地方因为它涉及大量的语义检索和模式匹配。2.2 为什么AI在Lean里能帮上忙传统上形式化证明的门槛极高你得同时懂数学、懂Lean的语法、还得熟悉Mathlib里成千上万个引理的名字和用法。一个熟练的Lean用户写一个中等难度的证明可能也要花上几天。AI的介入改变了这个成本结构主要体现在三个环节。第一是引理检索。当你要证明某个中间步骤时往往需要用到Mathlib里已有的某个引理但你不一定记得它叫什么。AI可以根据你的目标状态推荐可能用得上的引理名。第二是证明骨架生成。AI可以先给出一个大概的证明结构比如用归纳法还是反证法把大框架搭起来剩下的洞sorry由人来填。第三是错误修复。Lean报错信息有时候很晦涩AI可以帮你解读错误、定位问题、给出修改建议。提示AI生成的Lean代码几乎不可能一次编译通过把它当成高级自动补全而不是证明生成器心态会稳很多。2.3 费马大定理在Lean里的现状费马大定理的完整形式化是一个巨大的工程。它依赖的数学工具非常多包括模形式、伽罗瓦表示、椭圆曲线等这些在Mathlib里的覆盖程度参差不齐。所以现实中用Lean证明费马大定理往往不是一次性完成的而是分阶段推进先把依赖的基础理论形式化再逐步往上搭。这也是为什么热搜里说快速证明需要打个问号。更合理的理解是AI在某个具体环节、某个子目标的证明上显著加速了进度而不是一口气把整个定理拿下了。作为从业者看到这类标题时第一反应应该是去GitHub上看实际的commit记录和证明状态而不是被标题带着走。3. 从零跑通一个AI辅助Lean证明的完整链路3.1 环境准备Lean工具链的安装与版本坑Lean的安装方式这几年变过好几次目前主流是用elan来管理版本。elan类似于Rust的rustup可以让你在不同项目间切换Lean版本。安装命令大致如下curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh装完之后elan会自动把lean、lakeLean的构建工具类似cargo加到PATH里。这里第一个坑就来了Lean版本和Mathlib版本必须严格匹配。Mathlib更新非常频繁不同版本之间的API经常不兼容。如果你用了一个新版的Lean去编译一个旧版的Mathlib项目会报出大量莫名其妙的错误。正确的做法是在项目根目录的lakefile.lean或lake-manifest.json里锁定版本然后运行lake exe cache get lake buildlake exe cache get这一步非常关键它会下载预编译好的Mathlib缓存。如果不做这一步lake build会尝试从源码编译整个Mathlib那可能要几个小时甚至更久。我第一次搭环境时不知道这个硬生生等了一下午后来才发现有缓存这回事。3.2 把AI接进工作流编辑器与模型的选择Lean最常用的编辑器是VS Code配合lean4官方插件可以获得实时的目标状态显示infoview。这个infoview是形式化证明的核心界面它实时显示当前需要证明的目标goal和已有的假设hypotheses。AI的接入方式有几种。一种是用支持Lean的AI编程助手直接在编辑器里对选中的代码块提问。另一种是把当前的目标状态复制出来贴到对话式AI里让它给出下一步建议。我个人更倾向后者因为形式化证明的上下文很微妙把goal完整贴出来能让AI给出更准确的建议。这里涉及Token消耗的问题。Lean的goal状态有时候会很长尤其是当假设很多的时候。如果每次都把完整的goal贴给AIToken用量会迅速上升。一个实用的技巧是只贴关键假设把那些明显无关的假设省略掉既省Token又不影响AI判断。3.3 一个最小可复现的AI辅助证明示例假设我们要证明一个很简单的命题对于自然数nn 0 n。在Lean里写出来是这样theorem add_zero_demo (n : Nat) : n 0 n : by sorryby后面是证明策略tactic模式sorry是一个占位符表示这里还没证。把这段代码放进编辑器infoview会显示当前goal是n 0 n。这时候把goal贴给AI它大概率会建议用rfl或者Nat.add_zero。实际上Lean里这个命题就是Nat.add_zero这个引理本身所以直接写theorem add_zero_demo (n : Nat) : n 0 n : by rflrfl是自反性策略它会检查等式两边是否定义上相等。对于n 0和nLean的Nat.add定义里n 0会化简为n所以rfl能直接搞定。这个例子虽然简单但它完整展示了AI辅助的流程写goal → 贴给AI → 得到建议 → 验证。真实场景里的证明会复杂得多但流程是一样的只是迭代次数更多。3.4 迭代过程中的Token控制策略一个中等难度的证明可能需要几十次甚至上百次的AI交互。如果每次交互都消耗几千Token总量会很可观。我总结了几条控制Token的经验。第一保持对话上下文精简。不要在一个对话里塞太多不相关的内容证明到哪一步就开一个新的、聚焦的对话。第二优先让AI给策略名而不是完整代码。策略名通常很短比如induction、simp、omega让AI告诉你用哪个策略比让它生成一大段代码更省。第三善用Lean自己的自动化策略。Lean有一批强大的自动化策略比如omega能处理线性算术simp能化简aesop能做一定程度的自动证明。很多时候这些策略直接就能把goal干掉根本不需要AI。注意不要盲目相信AI给的引理名。AI有时候会幻觉出一个不存在的引理编译时会报unknown identifier。遇到这种情况去Mathlib的文档里搜一下真实的名字。4. 那些热搜标题不会告诉你的坑4.1 快速证明背后的真实工作量热搜说快速但形式化证明的快速和日常理解的快速不是一回事。一个在纸上几行就能写完的证明形式化之后可能要几百行因为每一步都要显式地引用引理、处理类型、展开定义。AI能加速的是其中的检索和试错环节但证明的整体结构设计、关键引理的拆解仍然高度依赖人的判断。我在实际项目里的体会是AI能把一个原本需要三天的证明压缩到一天但很难压缩到一小时。因为形式化证明的瓶颈往往不在想不出下一步而在想出了下一步但不知道怎么用Lean表达。AI能帮你解决后者但前者还是得靠人。4.2 GitHub上的证明项目怎么读如果你想验证某个AI证明费马大定理的说法最直接的办法是去GitHub上看项目。看的时候重点关注几个东西lakefile.lean里的依赖版本、sorry的数量、以及最近的commit记录。sorry的数量是判断证明完成度的关键指标。一个项目里如果还有大量sorry说明证明远未完成只是搭了个骨架。Lean甚至有个命令可以统计sorrylake exe sorry-count或者用grep直接搜grep -rn sorry --include*.lean .commit记录则能看出进展节奏。如果最近几周的commit都是小修小补说明项目卡在某个难点上如果突然有大量commit涌入可能是AI辅助起了作用。4.3 网络访问与依赖下载的现实问题做Lean项目绕不开从GitHub拉取依赖和缓存。实际网络环境下lake exe cache get和git clone可能会很慢甚至失败。常见的应对方式是配置镜像源或者提前把依赖下载好放到本地。这部分具体怎么配取决于你所处的网络环境我这里不展开但要有心理准备环境搭建本身可能就占掉整个项目三分之一的时间。另外Mathlib的缓存文件很大几个GB是常态。磁盘空间要留够不然下到一半失败会很崩溃。4.4 AI幻觉在形式化场景下的具体表现AI在Lean场景下的幻觉主要有三类。第一类是编造引理名比如它说用Nat.foo_bar但Mathlib里根本没这个引理。第二类是记错引理的参数顺序Lean对参数顺序很敏感顺序错了就编译不过。第三类是给出看似合理但逻辑不成立的证明步骤这种最危险因为它可能编译通过但证的是错的命题——不过好在Lean的内核会兜底逻辑不成立的证明最终过不了类型检查。应对幻觉的办法很简单每一步都编译验证。不要一次性让AI生成一大段代码然后才编译而是小步快跑生成一段就编译一次错了立刻回退。这样虽然交互次数多但总体效率更高。5. 把AI辅助Lean证明的经验迁移到其他场景5.1 这套方法论适用的边界AI辅助Lean证明的这套思路本质上适用于任何有严格验证机制的领域。因为严格验证意味着AI的错误会被立刻发现你不用担心它悄悄给你埋雷。反过来如果某个领域没有自动验证机制AI的输出就需要人工仔细审查效率优势会打折扣。具体来说形式化验证、类型系统设计、协议实现、密码学算法实现这些领域都有类似Lean的硬约束AI辅助的价值比较大。而像写业务文档、做产品设计这类没有唯一正确答案的场景AI更多是提供灵感验证成本高。5.2 从Lean项目里能学到的通用AI协作技巧即使你不做形式化证明从Lean项目里也能提炼出几条通用的AI协作经验。第一给AI明确的验证标准。在Lean里这个标准是编译通过在其他场景里你可以定义自己的标准比如单元测试通过、符合某个schema。有了明确标准你就能快速判断AI的输出是否可用。第二小步迭代优于大步跃进。让AI一次做太多事出错概率会指数上升。把任务拆小每次只让AI解决一个明确的问题成功率会高很多。第三保留人工判断的关键节点。AI可以帮你做检索、试错、补全但整体的方向判断、架构设计、关键取舍还是得人来定。把AI当成一个执行力很强但缺乏全局观的助手这个定位比较准。5.3 关于Token成本的实际账最后算一笔Token的账。一个中等规模的形式化证明项目如果全程用AI辅助Token消耗可能在几百万到上千万级别。按当前主流模型的价格这是一笔不小的开销。所以实际项目里通常是关键难点用AI常规部分用Lean自带的自动化策略这样能把成本控制在合理范围。我个人的做法是先用omega、simp、aesop这些自动化策略扫一遍能自动解决的就不麻烦AI剩下的硬骨头再交给AI并且尽量把goal精简后再贴过去。这样下来Token用量能比无脑全交给AI省下一大半。形式化证明这个领域AI的介入确实改变了游戏规则但它改变的是效率不是本质。费马大定理的证明依然是人类的数学成就AI做的是把它翻译成机器能懂的语言并且在这个过程中帮我们省下了大量重复劳动。看清这一点就不会被AI证明了费马大定理这种标题带偏也能更务实地把AI用在自己的实际工作里。
阅读完成 · 觉得有帮助？
