陶哲轩用Claude Code审查Mathlib代码风格实战演示

概述：AI在数学形式化中的「红队」角色

陶哲轩（Terence Tao）在最新视频中展示了一种与以往不同的AI使用方式。他将AI辅助工作分为「蓝队任务」（创造新内容）和「红队任务」（验证和审查已有内容），并认为AI在红队任务中表现更加出色。本次演示聚焦于使用Claude Code对Lean 4数学证明代码进行风格审查和优化，确保其符合Mathlib（Lean的核心数学库）严格的代码规范。

Lean 4是由微软研究院Leonardo de Moura团队开发的交互式定理证明器和函数式编程语言。与Coq、Isabelle等同类工具相比，Lean 4在性能和元编程能力上有显著提升。Mathlib则是Lean社区共同维护的核心数学库，目前包含超过15万条定理和定义，覆盖从基础代数到拓扑学的广泛数学领域，是目前世界上规模最大的形式化数学库之一。正因为体量如此庞大，统一的代码风格规范对于库的可维护性至关重要。

这项工作源于ISM Brown举办的分析形式化研讨会，团队选择了Riemann-Stieltjes积分作为形式化目标——这是一个在解析数论中有重要应用但尚未被Mathlib收录的概念。Riemann-Stieltjes积分由荷兰数学家Thomas Joannes Stieltjes于1894年提出，是Riemann积分的推广形式，将普通积分∫f(x)dx推广为∫f(x)dg(x)的形式，其中g是一个有界变差函数。这一概念在概率论（期望值计算）、泛函分析和解析数论中均有重要应用，例如在素数定理的证明中用于处理算术函数的求和问题，其缺席于Mathlib是一个值得填补的空白。

为什么Mathlib代码风格审查需要AI辅助

Mathlib的严格编码规范

Mathlib拥有极其详尽的代码风格指南，涵盖变量命名、行宽限制、输入结构、文档字符串格式、定理组织方式、空白处理等方方面面。此外还有专门的命名规范，例如le_of_forall_gt这样的命名约定，虽然初看像字母汤，但在包含数十万条引理的库中，统一的命名让人一眼就能猜出引理的内容。这套命名体系本质上是一种「可搜索的数学语言」——当你需要某个关于不等式传递性的引理时，你可以根据命名规律直接猜出它的名字，而不必翻遍文档。

陶哲轩坦言，他两周前首次向Mathlib提交了约300行代码，结果收到了数百条审查意见，其中大量是风格合规性问题。对于非资深贡献者来说，一次性满足所有规范几乎不可能。这也反映了数学形式化工作中「卫生工作」的普遍挑战：将非正式的数学证明转化为计算机可验证的严格符号推导，不仅要求数学正确性，还涉及大量工程性工作，包括选择合适的抽象层次、与已有库的接口对齐、满足编码规范等。这些工作虽然不涉及数学创新，却占据了形式化工作相当大的比例，也是许多数学家望而却步的原因之一。

AI代码审查的理想应用场景

这类机械性的风格检查正是AI的理想用例。陶哲轩表示：「我不想把时间花在检查空白要求上。让Claude在后台处理这些，而我专注于解决数学问题，这是很好的分工。」

实战演示：Claude Code的代码审查工作流程

前期准备：将风格指南转化为可执行规则

陶哲轩预先让Claude将Mathlib的网页版风格指南转换为Markdown文件，其中包含具体可操作的检查项，以及可通过Python脚本自动化的快速扫描规则（如列宽限制检查）。这一步骤本身就体现了AI辅助的价值：将非结构化的自然语言规范转化为结构化的可执行检查清单，为后续的自动化审查奠定基础。

机械性修复：自动化风格问题处理

Claude首先执行自动化扫描，发现的典型问题包括：

• 多余的空行：Mathlib规范要求段落间只有单个空行
• 冗余策略：如simp only在某些上下文中等价于simp，可以简化
• 代码压缩：将simp后跟exact的两行合并为单行exact调用

命名规范修正

一个典型案例是：代码中使用了viewpoint_integral.def作为方法名，但Claude检查Mathlib后发现，正确的命名应该是_def而非.def（因为def是Lean的保留字）。这类细微但重要的修正正是AI擅长的领域——它需要对整个库的命名惯例有全局了解，同时又要逐行检查代码，这恰好是人类容易疲劳出错而AI可以稳定执行的任务类型。

深层重构：Lean 4隐式参数优化

演示中最有趣的部分是Claude提出的一个中等难度重构建议：将某些引理的显式参数（b f g）改为隐式参数。

重构逻辑与收益

在Lean 4的类型系统中，参数声明方式直接影响代码的可用性。用圆括号()声明的显式参数需要调用者每次手动提供；用花括号{}声明的隐式参数则由Lean的统一化算法（unification）根据上下文自动推断，无需显式传入。此外还有双花括号[[]]声明的实例参数，用于类型类推断。隐式参数的合理使用是Mathlib代码风格的重要组成部分——过度显式会导致调用冗长，而过度隐式则可能让类型推断失败或产生歧义。

原始代码中，每次调用这些引理都需要显式指定b f g参数，但在大多数使用场景中，Lean的类型推断系统能自动推导出这些参数。将它们改为隐式（用花括号{}而非圆括号()声明）可以：

• 减少调用时的冗余代码
• 在少数无法推断的场景中，仍可通过@语法显式指定

执行过程与问题处理

Claude通过grep定位所有使用这些方法的文件，逐一修改签名和调用点。过程中遇到了类型推断失败的情况——某些上下文中Lean无法确定参数类型，需要显式标注。Claude能够识别这些问题并针对性修复。

说个细节，重构后Claude甚至发现了一个更简洁的证明：由于隐式参数为simp等策略提供了更多上下文信息，原本三行的证明被压缩为一行。这个意外收获揭示了一个深层规律：良好的参数设计不仅影响代码可读性，还会影响自动化证明策略的有效性，因为simp等策略依赖类型信息来搜索适用的引理。

Claude Code的技能积累与学习机制

Skill文件：项目知识的持久化

Claude Code维护一个独立的Markdown「技能文件」，记录：

• 代码库的结构特征（如积分代码的组织方式）
• 常见模式（如六种情况的分类讨论在该代码库中频繁出现）
• 踩过的坑（如忘记指定某些输入参数的教训）

这种机制本质上是在弥补大语言模型上下文窗口有限的天然缺陷。通过将项目特定知识外化为持久化文档，Claude在跨会话工作时能够快速恢复对代码库的「记忆」，而不必每次从零开始探索。这意味着随着使用时间增长，Claude会犯越来越少的重复错误，逐渐适应特定项目的编码习惯——形成一种类似「项目肌肉记忆」的效果。

局限性与人机协作边界

陶哲轩也坦诚指出了当前AI代码审查的局限：

1. 数学非平凡问题仍需人工：如证明「两个子区间上可积蕴含大区间上可积」这类数学上非平凡的引理，Claude要么失败，要么给出「非常丑陋的证明」，需要大量重构。这类引理往往需要对数学结构有深层直觉，而不仅仅是符号操作能力。
2. 跨文件重构的风险：修改参数签名导致多个文件构建失败，部分问题与当前重构无关（是之前未检查的遗留问题）
3. 人类判断不可替代：在Claude建议放弃某个修改时，陶哲轩注意到它其实可以修复但选择了回退——有时AI的保守策略并非最优。这反映了当前AI系统在「知道自己不知道什么」方面的局限：它可能低估自己的能力，在本可继续推进的情况下过早退出。

总结：AI辅助数学形式化的务实路径

这次演示展示了一种务实的AI协作模式：人类负责数学创造和架构决策，AI负责风格合规、机械优化和模式识别。这不是AI替代数学家，而是将数学家从繁琐但必要的「卫生工作」中解放出来，让他们专注于真正需要数学洞察力的问题。

从更宏观的视角看，这种分工模式可能对数学形式化领域产生