Claude 的数学形式化证明能力超预期

我们以能够亲自与所有感兴趣的合作伙伴、协作者和潜在客户建立联系为荣。请发送电子邮件，简要说明您希望以何种方式与 Galois 建立联系，我们将尽力在一个工作日内回复。

让我开门见山，不说任何关于外星人的废话：

Anthropic 推出的新 AI 编程智能体 Claude Code，非常擅长交互式定理证明（ITP）。

这让我非常惊讶，你或许也应该感到惊讶。

Lean 等交互式定理证明工具，是形式化方法工具中能力最强、可信度最高的一类。它们已被用于对密码学库、编译器和操作系统等重要事物进行形式化验证。遗憾的是，即使是专家，也会觉得 ITP 证明既耗时又容易出错。因此，发现 Claude Code 如此擅长 ITP，令人兴奋——也非常出人意料！如今，Claude Code 已经可以独立完成许多复杂的证明步骤，但仍然需要一位“项目经理”（也就是我）引导它完成整个形式化过程。不过，我认为 Claude Code 指向了这样一个未来：届时不再必须依赖专家，更多人都能使用定理证明器。

本文接下来的内容将深入探讨 Claude Code 到底能做什么。不过，如果你对自动推理或形式化验证感兴趣，我建议你先别往下读了，去注册 Claude Code、Gemini CLI、Aider、Codex 或其他某种编程智能体，然后用一个你非常熟悉的问题试试它。想用上真正有用的服务，每月大约需要 20 美元；如果想使用最先进的模型，可能需要每月 100 美元。我估计，只要投入大约两个小时，你就能取得一些令人惊讶的成功（也会遇到一些有趣的失败）。

（如果你真的这么做了，请给我发邮件，告诉我结果如何。）

交互式定理证明很难

在自动推理领域，存在一个深层次的权衡：限制底层数学的表达能力，往往会让推理更容易自动化；而增强其能力和通用性，则会让自动化变得更加困难。例如，SMT 求解器只能处理用一种简单逻辑语言表达的查询。也正因如此，SMT 求解器的行为足够可预测，可以作为 AWS S3 存储桶安全控制的一部分，每天运行十亿次。没有人需要在白板上写证明；求解器会快速且低成本地解决每一个定理。1

在光谱的另一端，交互式定理证明工具被设计得尽可能通用，以便我们能够用它们处理真正的数学™——例如费马大定理。遗憾的是，这种强大能力也使 ITP 工具出了名地难用。Nick Benton 在 2006 年写过一句令人印象深刻的话：“在刚开始使用 Coq 的那几周里，我几乎从未感到如此愚蠢和沮丧。”今年，我自学了 Lean——这已经是 Benton 写下那句话近二十年之后了。他当时指出的具体问题早已得到解决，但我仍然感到愚蠢和沮丧，程度远超我使用过的其他任何工具。

为什么 ITP 如此困难？有些原因非常明显：界面令人困惑、库不够丰富、文档质量不佳、错误信息难以理解。但这些并不是什么有趣的问题，而且无论如何，它们都正在得到解决。尤其是 Lean，在 Lean FRO 的专注投入下，正以惊人的速度不断改进。

更深层的问题是，ITP 会在多个方面带来很高的认知负担。即使人们并不总是明说，也能强烈地感受到这一点。它要求你像进行纸笔数学推导一样，同时处理多个抽象概念；愿意在 ITP 工具所使用的奇特语言中应付复杂的约束；还要能够忍受吹毛求疵到微观层面的严谨，而大多数人几乎不可能调动起这种耐心。

我曾开玩笑说，占主导地位的 ITP 策略是“PSMGS 集群”——由痛苦的研究生进行证明搜索（Proof Search by Miserable Graduate Students）。ITP 领域最令人瞩目的成果，往往是由极其聪明的人经过多年无比乏味的工作取得的：他们逐个案例、逐个案例、再逐个案例，缓慢地把每一个关键定理啃到只剩下一个小尖角。只有极少数天赋异禀的人能把这件事做好，但他们凤毛麟角，而且时间成本极其高昂。这对 ITP 工具的广泛应用构成了非常严格的限制，因为从成本收益角度算得过账的潜在项目少之又少。

定理证明不只是证明定理

遗憾的是，我并非天赋异禀（我只是个懒惰的笨蛋），所以我觉得学习 Lean 既烦人又困难。

于是，我开始寻找捷径。

SMT 求解器怎么样？Lean 对 SMT 提供了令人印象深刻的支持，其中包括新的 grind tactic。它奏效时确实很有用，但 SMT 只能处理范围极其有限的数学性质。hammer 等其他非 AI 自动化方法也类似：非常有用，但通常只适用于有限范围的问题。

都 2025 年了，AI 难道不能帮帮我吗？人们已经在 AI 数学领域开展了大量工作；我甚至还写过一些早期成果。我安装了最近几篇论文中经过微调的 AI 模型，用一些示例任务试了试，然后……没有一个真正帮上忙。2

我后来意识到，问题在于我选择的这些模型，是为了证明单个 Lean 定理而设计的。但这只是我使用 Lean 进行 ITP 时很小的一部分工作。在对一个理论进行形式化时，我通常会组合执行以下任务：

概念数学——思考我的理论需要哪些概念和定理

映射到 Lean——将我的概念转换成 Lean 的语法、类型和库

分解定理——将大型性质拆分成更小、更易于处理的引理

证明定理——实际使用 Lean 的 tactic 语言证明某个单独的定理（我找到的那些 AI 模型试图在这里提供帮助）

调试失败——弄清楚形式化内容为何被 Lean 拒绝

（我还可能执行其他任务。例如，我有时会使用 Plausible 编写基于性质的测试；而任何需要长期维护的证明，最终都需要更新和修复。）

这些任务之间经常存在来回拉扯。举个最近的例子：假设我想证明某个函数满足结合律（任务 4）。我意识到，因为选择了当前的底层类型，这个定理其实是错误的——糟糕（任务 5）。也许我可以通过换一种方式分解其他定理来绕开这个问题（任务 3）。但在这个案例中，我意识到结合律是一项硬性要求，因此必须将当前类型替换成其他类型——例如有限映射——然后据此重构整个形式化内容（任务 2）。我还需要检查自己的理论在数学上是否正确，或者我是否犯了某种概念性错误，导致重要定理根本无法证明（任务 1）。

我使用 Lean 时最令人沮丧的经历，很少与单个定理的证明有关。更常见的情况是，之前做出的某个决定出乎意料地堵住了我的路，而我必须在几种不同的复杂重构方案之间做出选择，才能解决问题。上面的例子就是如此——最终，我决定用有限映射重写所有内容，这意味着要重写多个定义和证明。

换句话说，Lean 的实际使用更像是围绕证明进行软件工程——也就是所谓的证明工程。单个定理的证明固然重要，但使用 Lean 时，许多工作都涉及选择抽象、重构代码、分析需求和修复失败等相邻任务。

好吧，我想，也许我需要的是某种不同的东西，更像是为软件工程而设计的 AI。

Claude Code 是一个 AI 编程智能体。没错，我一开始也不明白这是什么，所以让我解释一下。像 ChatGPT 这样的聊天机器人通常会接收一个请求，然后给出一个回答；而 AI 智能体可以将一个请求拆分成许多子任务，再逐一执行。这对软件工程尤其有用，因为一个大型任务可能需要阅读文档、修改文件、运行工具，等等。

更具体地说，你需要将 Claude Code 安装为命令行应用程序。它会弹出一个有点像 ChatGPT 的文本框，你在里面输入请求，然后由智能体处理。例如，你可以这样要求它：

“审查所有未提交的更改，并检查它们是否符合 ./README.md 中规定的提交标准。如果没有问题，就创建一个提交并推送它”

“为线程池选择一种表示方式，并编写合适的定义。确保该定义满足整个理论所需的全部性质，具体要求记录在 plan.md 中”

“定理 compose_is_assoc 似乎无法证明。你能找出原因并制定一个修复计划吗？请将计划记录在一份带时间戳的笔记中”

让我们看看最后一个请求，也就是要求修复 compose_is_assoc。Claude Code 可能会将任务拆分成以下步骤：

为自己编写一份 TODO 列表，说明如何完成这个请求

在本地代码库中搜索包含 compose_is_assoc 的文件

阅读文件中该定理周围的上下文

针对 <filename> 运行 Lean 构建系统，确认证明确实失败，并检查由此产生的错误信息

查找并阅读该定理所涉及类型的本地定义

查看标准库中 Lean 类型的在线文档

思考可能解决该问题的方法（有趣的是，ultrathink 是一个能够增加 AI 智能体“思考预算”的魔法关键词）

撰写回复，提出高层次的修复方案，然后请求用户授权编辑文件

重新运行构建，检查修复是否生效

（你可能会觉得，让 AI 智能体运行任意命令行工具简直危险得可笑。确实如此！默认情况下，每条命令都需要用户确认，同时用户可以配置白名单。然而，其中处处都是容易误操作的陷阱，我强烈建议不要拿自己在意的数据做实验。如何设计出能够安全、可靠使用的 AI 智能体，似乎是一个非常重要、却远未得到充分研究的问题。）

在幕后，上述每一步都可能涉及多次调用 Anthropic 托管在云端的 AI 模型。对于这种复杂请求，整个过程可能需要几分钟。作为用户，这其实可能有点无聊——你按下开始，然后看着 AI 智能体埋头苦干。

显然，AI 智能体会犯各种错误：语法错误、语义错误、概念错误。我的发现是，只要为它提供一个能够检测错误的工具，AI 智能体往往就能纠正这些错误。例如，假设我们想证明某个特定定理。通常，AI 智能体会创建第一个版本，然后进入循环：(1) 运行 lake build，检查当前证明能否通过；(2) 阅读错误信息；(3) 思考哪里可能出了问题；(4) 尝试修正错误。经过几轮迭代后，证明往往就正确了。

我认为，这正是 Claude Code 出人意料地擅长定理证明的部分原因。Lean 对它所接受的程序要求非常严格。这让人类编写 Lean 代码时备感艰难，但也意味着 AI 智能体能够获得详尽的反馈。在我看来，这表明我们或许应该针对 AI 智能体设计不同于人类使用方式的工具。与其试图避免失败，并且只输出经过高度处理、便于人类理解的信息，不如采用更严格的检查，同时生成更多关于问题所在的信息。

Claude 能编写 Lean

我使用 Claude Code，为一篇旧论文《Deny-Guarantee Reasoning》（Dodds、Feng、Parkinson、Vafeiadis，2009）编写 Lean 形式化。这篇论文在数学上并不算太复杂，但距离我上次研究它已经过去 15 年，我几乎忘掉了所有细节。该理论包括：

• fork-join 并发程序的简化形式模型

• 一种特殊的“权限”概念——它从逻辑上控制每个线程能够执行哪些操作

• 一套用于验证线程是否遵守其所分配权限的 Hoare 逻辑

• 大量关于线程、权限与逻辑之间如何相互作用的定理

我从一个空仓库开始，按照以下方式构建形式化：

• 我让 Claude Code 使用 Poppler，将研究论文和技术报告转换成纯文本。

• 我让 Claude ultrathink，编写一份形式化计划，其中包含一份全面的路线图，说明应该在什么时候形式化哪些内容。

• 我充当“项目经理”，指导 Claude Code 逐步执行研究计划。通常，我会先要求 AI 智能体“开始处理形式化计划的下一阶段”。

• 我要求 AI 智能体将定理定义与证明分开。定理的第一个版本使用占位证明（在 Lean 中写作 sorry）。然后，我会要求 AI 智能体在形式化计划的后续步骤中处理该证明。

• 每当取得任何能使构建干净通过的重大进展后，我都会要求 AI 智能体创建一个 commit。

• 除了少数例外情况（主要是棘手的解析错误），我避免亲自编写任何 Lean 代码。

令我惊讶的是，这种方法奏效了。你可以在 GitHub 上看到这个 Lean 项目。目前，我已经完成了形式化计划的大约 50%，总计有 2,535 行 Lean 代码，其中约 1,232 行是证明。

AI 智能体能够在我上面谈到的所有不同层级上工作，也能够判断何时需要在不同层级之间切换。我之前提到的有限映射重构，就是 AI 智能体替我完成的（尽管这已经接近其能力边界——它曾走进一条死胡同，而在第二次尝试时，我对它进行了仔细监督）。

Claude 有时也不会编写 Lean

先别太兴奋，这里有一个致命的注意事项：我认为，使用 AI 进行形式化比我手工完成要慢得多。让我解释一下。

作为 Claude 的“项目经理”，我的体验差异很大：

• 奇迹（很少见，但令人兴奋）——AI 智能体只用一轮迭代，就正确完成了一项庞大而复杂的任务。

• 缓慢推进（最常见的情况）——AI 智能体在第一轮迭代中大体走对了方向，但还需要与我进行一轮或多轮后续迭代才能完成。

• 原地打转（相当常见）——AI 智能体卡在某个错误上，反复尝试相同或相似的策略，却没有取得任何实质性进展。其中许多情况都涉及“爆炸半径”很大的改动，例如重新定义该理论使用的某个核心类型。

• 浅层持续性错误（比较少见）——AI 智能体犯了一个简单错误，却在多轮迭代中始终无法修复。许多这类错误都与解析有关，或许是因为解析错误包含的语义信息少于其他 Lean 错误。

• 深层持续性错误（很少见，但非常重要）——AI 智能体犯了一个我没有察觉的概念性错误，而且该错误没有引发构建失败。这些错误很难发现和修复，因为 AI 智能体通常会把自己的错误理解固化到注释中，并在之后的迭代中相信这些注释。

我发现，只需稍加提示，Claude Code 就能解决大多数错误。我也可以想象，如果 AI 智能体能够使用更好的工具，许多错误都可以避免，或者更快得到解决。例如，项目进行到大约一半时，我安装了 lean-mcp-lsp 包，它让 AI 智能体能够查询证明状态、搜索代码、运行测试代码片段，并使用其他一些小功能。Claude Code 证明定理的能力因此有了明显提升。我猜，这是因为它拥有了更多诊断错误和检验假设的方式。

最后一种错误，即深层持续性错误，虽然很少出现，但代价极其高昂。在这些情况下，AI 智能体自身已经陷入困惑，而且往往会进行大量改动，将这种错误理解嵌入其中。拆解它那些听起来似乎很合理的胡言乱语非常耗时。³ 在这些情况下，我的 ITP 经验绝对不可或缺，因为它让我能够退后一步，从整体上审视问题，而如今的 AI 智能体大多还做不到这一点。正是这些罕见错误的高昂代价，让我认为这个项目使用 AI 智能体完成所花费的时间，很可能比手工完成还要长。

对于这份形式化，我的信心也远不及它由专家完成时那么充分。定理经过了 Lean 检查，我认为我们应该对它们抱有很高的信任。但超过 60% 的 Lean 代码是定义，而不是定理。这些定义彼此足够一致，使我们能够证明关于它们的性质，这应该也能为我们带来一点信心。而且这些定义看起来相当合理，这又能再增加一点信心。但要想真正确定无误，我们必须仔细审计整个形式化，而这本身也将是一项极其艰苦的工作。在最理想的情况下，我们会拥有一小组显然正确的核心定义，但我怀疑，对大多数形式化而言，这根本不可能实现。

我很惊讶，你也一样

所以，Claude Code 能够编写 Lean 证明，这究竟有多令人惊讶？哦，旅人啊，让我们穿越时间的迷雾，前往那个遥不可及、令人难以想象的年份……响起摇曳的闪回特效……2024 年。

就在去年，如果你想用 Lean 对一篇论文进行形式化，你的选择是：(1) 去读研究生，学习如何亲自完成；(2) 期待为数不多的定理证明专家之一对你的问题产生兴趣；或者 (3) 放弃。当时并不存在什么被 AI 智能体取代的次优工具；这种能力压根就不存在。

更令我感到疯狂的是，Claude Code 并非作为定理证明工具而设计或推广的。我认为，它在这里取得成功，源于一些相关的 AI 能力——自主行动、长期规划、任务分解、软件工程和传统数学。Anthropic 很可能使用 Lean 数学基准来训练其模型；谁知道呢，也许他们还混入了一些随机的形式化方法问题。但我认为，也有可能我是最早将 Claude Code 应用于形式化方法论文的人类之一。

当然，上面我描述的实验并不是 Claude Code 从头到尾自动完成我的旧论文形式化。相反，这个智能体采取了一系列虽然各自令人印象深刻但相对独立的步骤，由我来评估结果，在必要时将其调整回正轨。这与 METR 的基准测试结果一致，该测试表明当前的 AI 智能体还不能执行非常长的任务。然而，METR 的结果也显示这种能力随着每个新 AI 模型的出现而快速增长。如果这一趋势继续，我们很快可能会拥有能够像人类专家一样好或更好地证明定理的 AI 模型，仅仅由于它们的原生能力。

即使 AI 没有变得更聪明，当 Claude Code 能够思考得更快时，它也会更有用。管理这个智能体目前有点令人沮丧，因为它涉及大量的闲置时间。每个请求需要大约 5-10 分钟才能完成，在此期间你做不了太多其他有用的事情，也不能轻易切换到另一项任务。

我认为也有一些简单的机会可以使今天的 Claude Code 更有效。添加 lean-mcp-lsp 带来了很大的改进，这表明即使简单的工具，如果它们给智能体提供更多信息，也会很有帮助。我们还可以让智能体访问我之前提到的那些以定理证明为重点的 AI 模型，并让智能体决定何时使用它们。我遇到的许多错误似乎是随机失败，我们可能通过并行运行多个智能体并选择表现最好的来避免它们。改进的门槛其实很低：在我的实验中，我做了我能想到最愚蠢的事，效果还相当不错。

何不尝试 Claude Code

在我从业以来，自动推理一直在缓慢发展。我们习惯了通过聪慧细致的工作实现的百分比级别的改进。Claude Code 打破了这种模式。即使它今天还有一些局限性，它也能做一些看起来在一年前似乎完全无法实现的事情。更令人吃惊的是，这种能力并非来自某种花哨的求解器或新颖的算法；Claude Code 根本不是为定理证明而设计的！

我认为 Claude Code 真正指向的是形式化方法面临的苦涩教训，就像在图像识别、语言翻译和程序合成这些领域中一样。从长远来看，我认为形式化方法的思想对于使 AI 驱动的证明成功至关重要。这是因为 AI 将需要许多与人类相同的工具来分解、分析和调试证明。但在那发生之前，我认为我们将看到许多我们珍视的聪慧细致的工作被没有特定领域专业知识的 AI 驱动的工具所淘汰。这个教训将是苦涩的，许多人正在抵抗它。

然而，我认为结果将值得这样的代价。ITP 从未被广泛采用的原因是，对大多数人来说，它的认知要求太高了。Claude Code 指向了一个定理证明不成问题的未来——便宜、充足且自动。我认为那将是一个美好的未来，如果它发生，我们应该为此做好准备，并知道接下来我们想解决什么问题。

进一步阅读 - Galois 实习生 Twain Byrnes 关于使用 AI 来推理 C 代码内存安全性的文章：Escaping Isla Nublar: Coming around to LLMs for Formal Methods

[1] 有一个合理的论点，认为人类历史上已被证明的所有不同定理中的很大一部分都是由 AWS Zelkova 访问控制工具证明的。

[2] 我不打算指出具体的论文，因为科学结果似乎很强，我对模型的评估非常不系统——实际上只是安装它们并四处探索。

[3] METR 最近发布了一项关于编码智能体的有趣研究，他们要求开源开发者完成 AI 辅助的工程任务。平均而言，开发者认为 AI 智能体提高了他们的生产力，但该研究表明他们的生产力实际上下降了。一个解释是，当前的 AI 智能体可以一致地使代码几乎正确，但要做到真正正确的差距比我们想象的要大。

‍T 503-626-6616E contact@galois.com

Portland, OR421 SW 6th Avenue, Suite 300Portland, Oregon 97204‍Arlington, VA901 N Stuart Street, Suite 501Arlington, Virginia 22203

‍Minneapolis, MN111 Third Avenue South, Suite 350Minneapolis, MN 55401‍Dayton, OH444 E 2nd StreetDayton, Ohio 45402

© Copyright Galois, Inc. 2024. All Rights Reserved | Terms of Use | Privacy Policy