用 Claude Code 给 Lean 证明做瘦身与风格校准

摘要

Terence Tao 演示了如何把 Claude Code 用作 Lean 代码的审查助手，重点不在生成新证明，而在检查已有代码是否符合 Mathlib 的风格、命名、可维护性和抽象层级要求。视频围绕 Riemann Stieltjes integral 的 Mathlib 形式化工作展开，展示 AI 如何发现空格、命名、参数隐式化、重复证明结构等问题，并在人类监督下完成小规模重构。

内容框架与概述

开头区分了蓝队任务和红队任务。蓝队任务偏向生成内容，例如写 Lean 证明；红队任务偏向验证、审查和修正，例如检查代码是否正确、是否符合风格规范。Lean 自带的类型检查器已经提供了强约束，所以 AI 生成 Lean 代码相对安全。但更适合 AI 的位置，是帮助人类检查那些繁琐、细碎、容易漏掉的规范问题。

视频中的具体案例来自一次分析形式化工作坊，目标是把 Riemann Stieltjes integral 补进 Mathlib。Mathlib 已经有 Lebesgue integral 和更抽象的 box integral，但缺少直接面向 Stieltjes 积分的接口。代码需要遵循 Mathlib 的高抽象风格，先在最大一般性下定义，再逐步导出常用情形。这种方式对教学不友好，但对大型数学库的复用和维护更高效。

Claude Code 被配置成一个代码审查助手，先读取 Mathlib style guide，再把规范转成可执行的审查清单。它能扫描空格、命名、行宽、重复证明模式、参数显式与隐式的取舍，也会把踩过的坑写进 repo 内部的技能文档。Tao 展示了 AI 有时能压缩证明、改善注释、发现更简洁的参数设计；也展示了 AI 仍会引入编译错误，需要 Lean 构建和人类判断兜底。

核心概念及解读

Blue Team Task，蓝队任务

指生成新内容的任务，比如让 AI 写 Lean 证明、生成数学代码或补全一批相似引理。这类任务看起来更有创造性，但风险也更大，因为生成结果可能类型正确，却结构臃肿、风格不合规，或者使用了不稳定的证明策略。

Red Team Task，红队任务

指审查、验证、攻击性检查的任务。这里的红队不是破坏代码，而是替人找问题。AI 在这类任务中很有价值，因为它不怕琐碎，可以反复查空格、命名、重复结构、风格指南和潜在重构点。人类则保留最终判断权。

Lean Type Checker，Lean 类型检查器

Lean 的类型检查器是数学形式化中的第一道硬门槛。只要代码不能通过类型检查，就不能算证明成立。它让 AI 参与证明生成变得更可控，因为错误会马上暴露。不过类型检查只能保证形式正确，不能保证代码优雅、可维护、符合 Mathlib 规范。

Mathlib Style Guide，Mathlib 风格指南

Mathlib 是 Lean 的核心数学库，规模巨大，所以必须有统一的命名、排版、文档和证明结构。看起来繁琐的命名规范，实际作用是让开发者能快速读懂陌生引理。没有这种约束，几十万条数学代码会变成难以维护的泥潭。

Golfing，代码瘦身

在这里指把 Lean 证明写得更短、更自然、更符合惯例。比如删除无效 rewrite、合并两行证明、减少重复变量声明、把显式参数改成隐式参数。好的 golfing 不是单纯压缩行数，而是在不牺牲可读性和稳定性的前提下减少噪声。

Implicit Arguments，隐式参数

Lean 中花括号里的参数可以由系统自动推断。视频里 Claude 建议把某些频繁出现的显式参数改成隐式参数，让使用这些引理时少写重复信息。这能让代码变短，但也可能让 Lean 在某些场景下推断失败，所以需要编译检查和局部修正。

文章基本信息

字段	内容
原标题	Golfing and stylistically aligning a proof using Claude Code
作者	Terence Tao
发布日期	2026 年 5 月 24 日

AI 在数学形式化中的角色分工

蓝队任务：生成内容

蓝队任务指让 AI 直接生产内容，比如写 Lean 证明、生成引理、补全数学代码。这类工作看起来更有创造性，也更容易吸引注意力。此前的相关演示，多集中在让 AI 寻找 Lean 证明，展示它能不能把某个数学命题写成可通过类型检查的形式化代码。

但生成证明只是一半。Lean 代码能通过类型检查，只说明它在形式层面成立，还不代表代码结构好、命名合适、风格稳定、适合进入 Mathlib。对于大型数学库来说，能跑只是最低门槛，真正麻烦的是后续维护、复用和审查。

红队任务：检查与审查

红队任务指让 AI 检查人类写出的内容，包括正确性、风格一致性、命名规范、代码结构、证明是否过于冗长、是否符合 Mathlib 的提交标准。这个位置更适合 AI，因为它擅长反复扫描、对照规则、找细小问题。

这里的 AI 不承担最终判断。它可以提出修改建议，也可以自动做一些低风险修补，但人类仍要看它是否把事情改对。Lean 的类型检查器提供了第一层安全网，构建失败时能立刻暴露问题。

Lean 类型检查器带来的安全边界

类型检查是最基本的验证工具

Lean 的类型检查器能马上发现 AI 生成的代码是否不成立。只要代码不能通过类型检查，错误就会显露出来。这个机制让 AI 参与 Lean 代码生成和修改变得相对可控。

不过类型检查器只管形式正确。它不会告诉你代码是否符合 Mathlib 风格，也不会判断某个证明是否易读，是否用了不推荐的 tactic，是否有重复变量声明，是否有多余 rewrite。这些更接近工程维护问题，需要额外审查。

AI 更适合补上风格审查这层

Mathlib 的贡献标准非常细：变量如何命名、行宽如何控制、文档字符串如何写、定理如何排版、空格如何处理、命名是否符合惯例。许多要求还没有完全自动化，只能靠人和已有 linter 一起检查。

这类工作枯燥，但对大型数学库非常关键。AI 在这里的价值不在于炫技，而是替人盯住那些容易分神、容易漏掉、又必须处理的细节。

Riemann Stieltjes integral 的形式化背景

Mathlib 里已有积分体系，但缺少直接接口

Mathlib 已经有 Lebesgue integral，也有高度抽象的 box integral。box integral 可以看成一种非常一般的 Riemann 型积分框架，能处理多维情况，也能容纳 Henstock integral 等更少见的积分形式。

问题在于，这套抽象框架还没有被专门特化成 Riemann integral 或 Riemann Stieltjes integral。Riemann integral 在很多场景可以被 Lebesgue integral 覆盖，但 Stieltjes integral 仍有独立价值，尤其在解析数论里经常需要对有界变差函数、分段连续函数，甚至复值函数进行积分。

Stieltjes 积分在当前 Mathlib 中有现实缺口

Mathlib 的 Stieltjes measure 相关构造主要处理非负测度，因此可以对单调函数做积分，但对复值函数、复测度支持不足。解析数论里常见的场景并不只限于单调实值函数，所以直接形式化 Riemann Stieltjes integral 有实际意义。

这个项目已经产生了几千行 Lean 代码，核心是基于 box integral 的 has_integral 谓词，定义 has_stieltjes_integral、可积性以及积分记号。由于 f 和 g 可以是向量值函数，定义层级被放得很一般。

Mathlib 的抽象风格

先最大一般性定义，再导出常用情形

Mathlib 的风格偏向基础效率。它倾向于先在足够一般的层面定义概念，然后再特化到常用场景。这样可以避免同一个概念在不同地方反复定义，也便于后续复用。

这和本科教材的写法差异很大。教材通常从标量函数、区间积分、具体例子开始，再逐步推广。Mathlib 更接近 Bourbaki 式路径：先把基础抽象搭好，再让具体场景成为抽象结构的特例。

对学习不友好，但对大型库维护有效

这种写法初看不直观，甚至显得繁琐。可是当一个数学库有几十万条引理时，统一抽象和统一命名会变成阅读效率的来源。你看到一个引理名，就能大致猜到它在说什么、输入是什么、结论是什么。

这也是 Mathlib 风格指南存在的原因。它不是单纯追求排版整齐，而是在让整个库保持可搜索、可猜测、可组合。

Mathlib 风格指南的审查压力

初次提交会遇到大量细节反馈

即便是几百行不算大的提交，也可能收到大量 moderator 评论，其中一部分是数学内容，另一部分是风格问题。比如命名是否符合惯例，行宽是否合适，空格是否正确，docstring 是否够规范， theorem 结构是否符合库内习惯。

这说明进入 Mathlib 不是只要证明成立就够了。代码还得像 Mathlib 的代码。这对新贡献者压力很大，因为规则多，细节密，第一次很难全部命中。

AI 可以把风格指南转成审查清单

Claude Code 被用来读取 Mathlib style guide，并把其中规则整理成 markdown 形式的审查清单。这样 AI 不只是泛泛地看代码，而是带着具体规则去扫文件。

它可以做一些机械检查，例如多余空行、错误空格、不必要的 simp at *、可合并的证明步骤、命名是否接近库内惯例。这些小问题单个看不大，但堆在一起会影响提交质量。

Golfing：证明瘦身与表达优化

瘦身不是单纯压缩代码

Golfing 在这里指把 Lean 证明写得更短、更自然、更符合 Mathlib 惯例。比如把两行 simp 加 exact 合成一行，把无效 rewrite 删除，把重复变量声明上移到统一 block，把多余参数省掉。

好的瘦身必须保留可读性。Claude 曾建议某些六分支 case split 也许能用循环对称性压缩，但压缩后证明会更难读，于是保留原结构反而更合适。短不是唯一目标，清楚和稳定更重要。

有些地方最好的修改就是不改

在 Stieltjes 积分的区间拆分证明中，代码需要处理 $a$、$b$、$c$ 的不同顺序。相等情形容易通过积分从一点到自身为零来处理，剩下还有六种严格顺序。Claude 检查后没有强行改写，而是接受当前结构，并建议改进注释，说明为什么需要这六种情况。

这点很关键。AI 审查工具不能只会把代码改短，还要能识别哪些地方结构虽然笨重，但数学上透明、维护上安全。

Stieltjes 积分中的区间方向问题

从正向积分扩展到反向积分

项目先定义从 $a$ 到 $b$ 且 $a < b$ 的有序积分，然后再把积分扩展到反向区间。从 $b$ 到 $a$ 的积分通过取负来定义。这样用户既能向前积分，也能向后积分。

这个设计让 API 更自然，但证明会变复杂。许多定理需要先证明有序版本，再证明一般版本。比如加法性、线性性、区间拆分，都要考虑方向变化。

区间拆分需要处理多种顺序

基本公式是从 $a$ 到 $c$ 的积分等于从 $a$ 到 $b$ 的积分加上从 $b$ 到 $c$ 的积分。若 $a < b < c$，证明相对直接，可以借用 box integral 里已有的拆分引理。

但一般情况下，$a$、$b$、$c$ 不一定有序。$b$ 可能在中间，也可能在左侧或右侧。为了得到完整 API，就必须处理所有顺序情况。这类证明数学上不深，但形式化时会很繁琐。

有界变差函数与连续函数的关键定理

连续函数对有界变差函数积分

后半部分涉及一个关键定理：如果一个连续函数对一个有界变差函数积分，那么 Stieltjes 可积性成立。这是整个形式化工作中的重要基础结果。

表面上，非形式化教材可能只用几页附录就能讲完。Tao 提到参考的是 Montgomery Vaughan 教材中的短附录。但搬进 Lean 后，工作量明显放大，因为每个直观步骤都要变成精确对象和可检查证明。

直观排序也需要大量形式化代码

非形式化文本里可以说，把区间分割按大小顺序排列，得到点列 $x_1$ 到 $x_n$，每个小区间夹在相邻点之间。人在图上一看就明白。

Lean 里不能靠图像直觉。要证明这些子区间确实可以排序，要说明它们如何覆盖、如何不交、如何对应到点列。这个步骤本身就需要几百行代码。形式化数学最大的成本，往往藏在这些平时被省略的显然步骤里。

Claude Code 的 repo skill 机制

项目级记忆帮助减少重复错误

Claude Code 维护了一个 repo 内部的 markdown skill 文件，记录这个积分代码库的结构、常见模式、风格要求和踩坑经验。比如某些拆分证明经常出现六种顺序情况，某些引理需要显式补参数，某些命名需要遵守 Mathlib 惯例。

这相当于给 AI 建立项目记忆。它不再每次从零开始审查，而是逐步积累本仓库的局部规则。用得越久，越能少犯以前犯过的错。

Gotchas 比抽象说明更有用

skill 文件里最有价值的部分，是那些具体踩坑记录。比如某个引理如果不写明某些参数，Lean 无法推断；某种 tactic 改写看似可行，但会导致构建失败；某类 refactor 会影响其他文件。

这些记录比泛泛的风格建议更实用。因为它们直接来自本项目的失败经验，可以转化成下一次审查时的预警。

显式参数与隐式参数的取舍

显式参数让调用更啰嗦

一些基础引理原本带有显式参数，例如 $B$、$f$、$g$、$L$。在许多调用场景里，这些参数其实可以由上下文推断出来。反复写它们会让证明显得臃肿，也会增加修改成本。

Claude 建议把部分参数改为隐式参数。这样多数调用可以少写一批参数，代码更短，也更符合 Lean 中常见的 API 设计方式。

隐式参数会带来新的推断问题

改成隐式参数后，一些地方会变短，甚至会让原本三行的证明变得更简单。因为多个引理组合在一起时，上下文足够丰富，Lean 能自动填洞。

但也有相反情况。某些地方 Lean 推断不出 $a$ 和 $b$，就必须重新显式指定。还有些文件会因为引理签名变化而暂时构建失败。这个过程说明，API 重构不能只看单个文件，要跑整个项目构建。

AI 自动修改的边界

小修改可以自动化

空格、空行、简单 proof golfing、注释调整、删除显然冗余的步骤，这些低风险修改可以让 Claude 自动完成。只要 Lean 构建能兜底，人类可以把注意力留给数学结构和 API 设计。

这种分工很现实。人类不该把大量精力消耗在检查空格和压缩两行代码上，AI 可以承担这部分疲劳劳动。

复杂错误仍要人类接管

在构建其他文件时，Claude 发现某个文件出问题，但那个问题和当前 refactor 没有直接关系，而是来自此前对一维 box 结构和记号系统的改动。Tao 很快判断这需要自己手动处理，因为 AI 可能会被错误来源带偏。

这说明 AI 适合发现问题、局部修补、给出候选方案；当错误牵涉到设计历史、数学意图和多文件结构，人类仍然要介入。尤其是形式化数学代码，很多失败不是语法问题，而是抽象设计留下的连锁反应。

可维护性高于一次性通过

Mathlib 代码要为未来读者服务

进入 Mathlib 的代码不是一次性脚本。它会被其他证明调用，被后续开发者阅读，被 API 继续扩展。所以代码要尽量模块化，避免高级结果直接依赖底层实现细节。

视频中提到，基础引理应该集中在底层使用，后续复杂结果应尽量通过更稳定的 API 访问。这样底层签名变化时，影响范围会小很多。

编译通过只是开始

Lean 代码能通过构建，只说明它没有形式错误。要进入 Mathlib，还要经过风格、结构、命名、抽象层级、API 可用性等审查。AI 参与的重点恰好在这些编译器不完全覆盖的区域。

这也解释了为什么 AI 工具在数学形式化中的价值，不能只用能不能自动证明定理来衡量。它还可以成为维护大型数学工程的助手，帮人把代码从能跑推进到适合合并。

对 AI 编程工作流的启发

AI 最适合做持续陪审员

这套工作流的核心，不是让 AI 一口气写完数学库，而是让 AI 持续陪审。人类写出核心内容，AI 对照规范检查，提出小修，运行构建，记录失败经验，再把经验带回下一轮审查。

这和普通编程里的 code review 很像，只是 Lean 的审查层更细，因为代码本身就是数学证明。AI 在这里像一个不知疲倦的初筛 reviewer，负责把大量低级问题挡在正式提交之前。

人类保留数学判断和设计判断

AI 可以发现一处证明能短一行，也可以建议把参数改为隐式，还能扫出命名问题。但是否引入新引理、是否改 API、是否保留六分支 case split、是否值得证明 converse lemma，这些仍然需要人类判断。

尤其是数学上有难度的引理，贸然让 AI 生成可能得到很难维护的证明。更好的做法是把 AI 放在辅助位置，让它减少噪声，而不是替代数学设计。