文章目录Lean形式化证明技术解析从费马大定理到可检查的AI数学工程一、引言二、纵向发展数学为何需要另一种证明语言2.1 从页边空白到庞大的依赖网络2.2 从人工编码到模型辅助构造2.3 这次突破为何依赖协作平台三、核心原理候选证明如何变成机器可以接受的对象3.1 命题、类型与证明项3.2 内核正确不代表题目一定写对3.3 公理与占位符必须进入审查范围四、工程架构让数万个定理能够协同推进4.1 用依赖图代替不断变长的聊天记录4.2 声明与证明分离为何有价值4.3 并行的代价来自接口冲突4.4 代码规模不能直接代表数学贡献五、工程实践如何启动一个可复查的形式化项目5.1 先选择能够完成验证的目标5.2 建立三种互相独立的验收材料5.3 将失败信息转成可处理的任务5.4 预算应按有效节点计算5.5 用一个算法性质理解形式化验收5.6 构建速度与可信边界需要分别优化六、横向对比Lean、其他证明助手与传统验证路线七、落地判断验证速度提高之后瓶颈会移向哪里7.1 从写证明转到定义正确的问题7.2 验证吞吐增加会改变研究产物的形态7.3 将失败成果也变成可复用知识八、总结Lean形式化证明技术解析从费马大定理到可检查的AI数学工程一、引言数学证明最令人紧张的时刻有时发生在论文写完之后。一个推导看起来流畅同行也觉得方向合理却可能在几十页之前漏掉了某个适用条件。后面的每一步都认真完成最终结论仍然站不住脚。人工智能能够快速生成证明文字之后这个老问题变得更加尖锐谁来检查不断增加的推理产物2026 年 9 月 4 日Anthropic 发布费马大定理形式化研究称 Claude 在约 11 天内基本自主完成端到端机器检查证明产出约 1300 万行 Lean 代码最终证明使用了约 29500 个中间定理。[1] 这些数字来自发布方本文没有重新编译整个工程也不把它们理解为一般数学任务的固定效率。亲爱的朋友们创作不容易若对您有帮助的话请点赞收藏加关注哦您的关注是我持续创作的动力谢谢大家有问题请私信或联系邮箱jasonai.fngmail.com这项工作的对象是已有数学证明的形式化。它沿着怀尔斯证明及后续整理的路线把数学家能够阅读的论证转成证明助手能够检查的对象。理解这一点才能避免把“首次完成机器检查”说成“人工智能首次证明费马大定理”也才能看清真正的工程突破。时效说明截至 2026-09-07。项目规模、耗时与模型描述依据 Anthropic 原文架构解释结合 Lean 的通用原理。本文的验证流程属于工程建议不是对该仓库独立复现成功的声明。二、纵向发展数学为何需要另一种证明语言2.1 从页边空白到庞大的依赖网络费马大定理的命题很短当整数指数大于二时不存在满足相应幂次方程的正整数解。短命题并不意味着短证明。怀尔斯在 1993 年公布证明后审查发现关键缺口经过与理查德·泰勒合作修补相关工作在 1995 年发表。这个过程说明顶尖专家的理解和严密的逐步验证仍然是不同任务。现代数学不断复用此前积累的结论。论文里一句“由标准结果可得”可能依赖一整套代数、几何和数论知识。读者能够在脑中补齐一部分条件但计算机没有这种默契。它需要知道对象属于什么类型、映射保持什么结构以及使用定理时所有前提是否成立。因此形式化的工作量不能按论文页数估算。文章只写出值得向同行解释的部分机器证明还要补上同行通常自动理解的背景。把一个著名定理形式化往往意味着同时建设此前没有完成的基础设施。2.2 从人工编码到模型辅助构造证明助手并不是大型语言模型时代才出现的工具。长期以来研究者已经利用交互式证明系统表达逻辑、程序性质和数学定理。Lean 与 Mathlib 的价值在于让相互依赖的数学定义与证明逐步积累为可复用的软件工程。[2][3]2024 年启动的 Kevin Buzzard 团队项目代表了社区对费马大定理形式化的系统推进。它的重要性不仅在于最终是否首先完成目标还在于提出蓝图、组织定义、识别缺失的数学组件。Anthropic 原文也明确致谢这一社区项目及其他已有工作没有把基础设施算作模型从零创造。大型语言模型改变的是候选构造的速度。过去人需要频繁查找库里的引理尝试策略解释报错再修正表达现在模型能够承担大量这样的循环。但证明检查的标准没有因此降低。模型提出的代码仍须经过同样的逻辑检查流畅的解释也不能替代内核接受。2.3 这次突破为何依赖协作平台研究原文披露早期尝试已经取得局部成果却因为代理逐渐丢失项目状态、协作失效而停滞。转向 Prove2Me 后定理依赖被表示为有向无环图系统能区分哪些前置条件已经完成哪些工作可以继续推进。[1][4]这里的转折点很具体瓶颈从“会不会写一段证明”转到“如何让数万个证明持续组合”。当工程规模扩大模型上下文不再适合独自承担项目数据库。显式依赖、可查状态与可重用结果让一次次局部推理变成累积工作。三、核心原理候选证明如何变成机器可以接受的对象3.1 命题、类型与证明项理解 Lean 可以从一个简化关系开始命题对应类型证明对应这个类型的对象。写出定理声明相当于规定最后必须构造出什么证明过程中产生的表达式最终要满足这份类型约束。真实系统还有宇宙层级、归纳类型、定义展开等细节但这个关系足以说明为何自然语言的自信不能决定结果。例如某个策略可以自动处理算术等式。策略成功的意义不是它输出“我确认成立”而是生成能够被检查的证明。复杂搜索可以在外层发生检查层仍保持相对小而明确。这是形式化系统在可信性上的关键分工。-- 教学示例展示命题与证明不涉及费马大定理工程。 theorem equality_transitive (a b c : Nat) (hab : a b) (hbc : b c) : a c : by exact Eq.trans hab hbc这个例子并不复杂却揭示了一个约束前提必须明确存在。模型不能在缺少a b时靠文字说服类型检查器也不能因为结论看起来合理就跳过对象之间的关系。3.2 内核正确不代表题目一定写对形式化系统检查的是编码后的命题。假设业务要求证明一个函数对所有输入安全而形式化声明无意间把输入限制为空集合系统可能给出完全合法但毫无业务意义的证明。数学项目同样可能在定义、量词或假设层面偏离原目标。所以验证至少分两层一层检查证明是否符合逻辑规则另一层检查形式化命题是否忠实表达目标。Anthropic 原文提到使用比较器确认最终声明与 Mathlib 对费马大定理的声明一致。这一步和 Lean 检查本身互补不能省略。3.3 公理与占位符必须进入审查范围证明助手不是摆脱所有假设的神奇机器。项目使用哪些公理、是否引入新的未经证明声明、是否遗留占位符都直接决定最后“已证明”的含义。原文表示最终证明只使用 Lean 的三个标准公理这里应理解为发布方报告的公理依赖结果而不是“没有任何基础假设”。检查对象回答的问题单独通过仍可能遗漏什么编译与内核检查证明项是否满足形式规则命题可能编码错误定理声明比较是否证明了目标命题依赖中可能多出假设公理依赖审计结论建立在哪些基础上工具链与构建环境问题干净环境重建他人能否重复得到结果人类仍需理解数学含义严格的交付不能只放一张成功截图。它应保留入口定理、依赖版本、构建命令和验证结果让下一位研究者能够沿同一条路径检查。四、工程架构让数万个定理能够协同推进4.1 用依赖图代替不断变长的聊天记录Prove2Me 的核心组织方式是把定理声明放进依赖图。一个节点可以包含形式化声明、自然语言说明、前置节点以及当前证明状态。工作者领取可推进的节点而不是从一段越来越长的对话里猜测“大家做到哪里了”。Human mathematical blueprint | v Theorem DAG --- Ready-node scheduler ^ | | v Verified library --- Candidate proof workers ^ | | v ---------- Lean compilation and checking | v Final statement axiom audit图中的调度器不能把“某工作者说完成”当作节点完成。节点状态应由实际检查结果推进依赖发生变化时后续节点还需要重新验证。否则系统会产生一种危险的表面繁荣大量任务显示绿色最终目标却建立在已经失效的接口上。4.2 声明与证明分离为何有价值原文介绍平台将定理声明和证明拆开维护以改善编译速度和资源消耗。可以把声明理解为稳定接口证明理解为具体实现。其他工作者在接口确定后理解自己需要的结论不必反复吞入所有证明细节。但这种分离不能让未完成依赖冒充已验证结果。工程上需要清楚区分“声明已登记”“可暂时据此规划”“证明已检查通过”。最终交付必须把所有需要的证明重新连接起来而不是只展示一张计划图。4.3 并行的代价来自接口冲突多个工作者同时证明不同引理确实可以利用并行计算。然而如果两组分别用不同定义描述同一个数学对象后续会付出转换成本。一个团队把同构当作等式使用另一个团队保留结构映射单看各自文件都合理组合时就可能卡住。这使得共享定义的审查比任务数量更重要。基础对象的命名、参数顺序、隐式实例和约束条件应由维护者建立相对稳定的约定。能够复用已有 Mathlib 定义时通常值得优先复用自行创建近似对象可能让局部工作更快却拖慢整个工程。4.4 代码规模不能直接代表数学贡献1300 万行是值得关注的工程规模但不等于同等数量的新数学洞见。发布方也说明机器生成证明可能比经过社区维护的 Mathlib 更冗长。自动化策略展开、重复辅助引理和代码组织方式都会影响行数。评价成果应看哪些关键依赖已经被可靠处理证明是否便于复用以及维护者能否理解接口。将相同结论压缩成更清晰的库组件可能没有新的发布数字却更有利于未来数学工作。五、工程实践如何启动一个可复查的形式化项目5.1 先选择能够完成验证的目标普通团队不宜把费马大定理的资源投入当作起步门槛。更可行的入口是已经有人类证明、定义相对稳定、依赖库较成熟的小型结果。比如一个组合恒等式、一段算法的局部不变量或者课程讲义中的一组引理。第一份交付应同时包含自然语言命题和形式化声明。领域专家先检查二者是否一致再让模型大规模尝试证明。把题目表达错误留到最后会让后续所有自动化加速都变成返工加速。5.2 建立三种互相独立的验收材料第一种是可读说明解释为何要证明这个结论、主要依赖是什么。第二种是可构建工程固定 Lean 和依赖库版本。第三种是审计结果记录入口定理、公理依赖、占位符检查和干净环境重建情况。formalization/ lean-toolchain lakefile.toml Formalization/ Definitions.lean Lemmas.lean MainTheorem.lean docs/ statement-map.md dependency-notes.md verification/ build-log.txt axiom-report.txt这是推荐的工程布局不是官方仓库目录。文件组织的目的是让证明结果能够离开最初的聊天会话交给另一个人复查。5.3 将失败信息转成可处理的任务编译错误可以来自缺少实例、命名空间错误、类型不匹配也可以来自真正的数学缺口。把整段日志原样反复送给模型容易浪费上下文。更有效的方式是记录最小失败位置、当前目标、可用前提和最近修改并保留完整日志供追查。如果模型连续尝试同一种无效策略应暂停该节点并重审声明。错误可能在数学拆分层面而不在战术搜索层面。比如一个引理缺了有限性假设再多局部重试也不会补出正确证明。5.4 预算应按有效节点计算官方项目消耗约六十亿输出 token使用的是大致可比于 Claude Fable 5.1 的内部通用研究模型。[1] 这一口径不能直接转换成公众订阅计划的成本也不能假设公开模型在相同时间内完成同样工作。试点可以记录每个节点的尝试次数、编译耗时、实际接受的证明以及人工修正原因。这样能够识别哪些工作值得继续自动化哪些定义需要专家提前整理。仅统计模型写了多少行代码会鼓励制造重复证明和不必要的辅助结构。5.5 用一个算法性质理解形式化验收设想团队希望证明一个库存扣减函数不会产生负数。自然语言要求看起来简单但形式化之前至少要回答库存用自然数还是有符号整数表示缺货时返回错误还是扣成零并发请求是否属于模型范围。若只证明自然数结果非负这个性质可能由类型定义直接成立却没有说明系统是否正确拒绝超额购买。更有意义的规格需要同时表达成功与失败条件库存充足时新库存等于原库存减去购买数量库存不足时不产生扣减结果错误路径不改变已有状态。若还有并发必须进一步描述两个操作怎样排序。这个例子说明证明难度与业务价值不由命题长度决定而由规格是否覆盖真实风险决定。让模型参与时可以先请它列出可能存在的歧义再由人确认定义随后构造证明。模型提出的新前提必须显式审查不能为了让证明容易通过而增加“所有请求都合法”之类过强假设。否则系统证明的只是理想世界中的性质。5.6 构建速度与可信边界需要分别优化大型形式化工程可能大量使用编译缓存。缓存能够减少重复检查时间但对外发布时仍应说明哪些部分重新构建、哪些部分来自固定依赖确保独立验证者能够从可信入口重建。一次增量构建成功与从干净环境完成全量检查提供的证据强度不同。依赖升级后也需要重新观察证明行为。库中同名定理的接口变化可能造成直接编译失败定义细节变化还可能影响对目标命题的理解。维护者应把语言版本、库版本和最终声明一起记录避免只保留一个模糊的“最新版可运行”。对于需要长期保存的成果可在发布包中附上可读的依赖摘要、入口定理说明和最小复查步骤。这样即使完整工程规模很大读者也能先知道信任建立在哪里再决定投入多少资源重建。形式化提高了验证的可执行性却仍需要良好的技术写作帮助人找到正确入口。六、横向对比Lean、其他证明助手与传统验证路线形式化项目有多条成熟路线。选择不应只看模型最近在哪个工具上演示成功还要看领域已有库、团队知识和最终验收对象。路线核心方式常见选择理由主要投入Lean 与 Mathlib依赖类型与可检查证明项数学库复用、现代交互工具定义对齐、库知识、编译维护Rocq交互式证明与程序形式化已有验证项目与提取工具链专门语言和既有组件学习Isabelle/HOL高阶逻辑与自动化证明支持成熟理论库、结构化证明理论组织、自动化配置SMT 求解器针对约束片段自动求解有界性质、程序条件检查建模范围、求解复杂度人工同行审查专家理解与批评论证新概念、解释价值和数学意义人力、时间和审查一致性Lean 的吸引力首先来自已有数学工作的积累。当目标用到的对象在 Mathlib 中已经表达得很好模型可以检索并拼接现有结果。若另一个证明助手里已有完整领域库仅为追随热点迁移可能意味着重新承担多年基础建设。SMT 适合处理它擅长的逻辑片段但把一个大型数学证明交给通用求解器并不意味着它能自动完成全部定义和高层构造。反过来在简单边界检查中动用大型交互式形式化工程也可能过度增加维护负担。人工审查仍然负责一些不同层次的问题。一个机器证明可以告诉我们某个形式化结论成立却不能独自决定它是否值得研究、解释是否具有启发性、定义是否体现原问题。形式化更像为审查提供坚固的逻辑底座使人能够把注意力放到数学意义上。关于使用口碑本文掌握的是发布方披露与被引用专家的评价不是大规模用户调查。Buzzard 对成果的积极评价具有专业价值但它不能推出所有数学家已经接受同一种自动化工作流。采用效果仍取决于研究方向和形式化成熟程度。七、落地判断验证速度提高之后瓶颈会移向哪里7.1 从写证明转到定义正确的问题当机器能够更快完成局部证明前置的命题整理会变得更重要。研究者要决定哪些概念值得沉淀、如何表达共同假设以及怎样避免相近定义反复出现。这类工作不会因为生成速度提高而消失反而更影响整个项目的扩展效率。代码团队也能从中得到启发。若把规格说明写得含糊然后让模型自动实现并证明系统可能只证明了一个错误规格。形式化的高价值来自“人类目标到精确定义”的映射而不是单独增加验证工具。7.2 验证吞吐增加会改变研究产物的形态可以预期部分数学成果会同时提供面向人的论证和面向机器的工程文件。前者解释结构后者承担细节检查。两种产物长期共存比只剩代码或者只剩文字更容易满足不同读者的需要。不过这仍是趋势判断。大型项目的编译资源、依赖维护和长期存档成本不会自动归零。若每篇论文都带来一个难以重建的庞大仓库形式化也可能制造新的审查积压。因此公共库维护和构建规范需要与生成能力同步发展。7.3 将失败成果也变成可复用知识某个定理最终未能完成不意味着过程没有价值。错误的候选可以帮助发现缺失假设重复失败可以揭示库接口不好用依赖图可以显示某个基础领域尚未充分形式化。前提是这些信息被整理成明确材料而不是埋在海量会话日志里。团队应该保存失败原因的分类却不必永久保留所有无效草稿。真正可复用的是已验证的局部引理、定义映射和可重现的反例。这样的积累能让下一次尝试从更高起点开始也能避免机器反复探索同一条死路。八、总结费马大定理项目揭示了一个很有工程意味的变化生成能力与验证能力分开设计之后自动化系统可以承担比单次对话大得多的工作。模型搜索候选平台维护依赖Lean 检查证明人类审查问题定义和数学意义各层职责相互补充。观察角度本文结论历史位置延续多年形式化建设利用模型加速候选构造技术关键证明内核、命题一致性、公理审计与依赖调度工程瓶颈共享定义、编译成本、接口稳定和长期维护采用方式从可复查的小目标开始积累可靠的数学组件纵向看形式化始终在解决“如何把人理解的理由交给机器检查”横向看不同工具的优势来自逻辑基础、成熟库和应用场景。两条线交汇后最值得关注的不是某次生成的规模而是已经验证的知识能否不断被下一项工作复用。人工智能让证明候选更加充足也让验证基础设施更有价值。对于研究者和工程师可靠的起点是把目标写清楚把依赖固定下来把结果交给独立检查。这样生成速度的提高才会转化为能够长期保存和累积的知识。参考资料Formalizing Fermat’s Last TheoremAnthropicLean 的费马大定理项目介绍形式化证明公开仓库AnthropicProve2Me: An Open Collaborative Platform for Scaling Math Formalization