陶哲轩用Claude Code做数学证明审查：红队任务比蓝队更有价值

概述：AI在数学形式化中的新角色

数学家陶哲轩（Terence Tao）近日发布了一段演示视频，展示如何使用Claude Code辅助数学形式化工作。与以往使用AI生成Lean证明代码（"蓝队任务"）不同，这次他重点展示了AI在"红队任务"中的应用——即由人类编写代码，让AI负责审查、校验和优化。

**红队（Red Team）与蓝队（Blue Team）**的概念源自军事和网络安全领域：红队负责模拟攻击、发现漏洞；蓝队负责防御和验证。在AI安全领域，红队测试已成为评估大型语言模型安全性的标准方法。陶哲轩将这一框架引入数学形式化，用红队指代验证和审查工作，蓝队指代创造性生成工作，这一类比直观地揭示了两类任务在风险特征和所需能力上的本质差异。

陶哲轩明确区分了两类任务：蓝队任务是创造性工作，如编写新的Lean证明；红队任务则是验证和检查工作，确保代码的正确性和风格合规性。他认为AI在红队任务中的价值甚至超过蓝队任务，因为这类繁琐但必要的工作正是AI的理想应用场景。

背景：Mathlib的Riemann-Stieltjes积分形式化

这项工作源于上周在布朗大学ISM举办的分析形式化研讨会。与会者分组选择了Lean中央数学库（Mathlib）中尚缺失的分析学主题进行形式化。陶哲轩所在小组选择了Riemann-Stieltjes积分。

关于Lean与Mathlib：Lean是由微软研究院Leonardo de Moura开发的交互式定理证明器和函数式编程语言，其核心设计目标是让数学证明可以被计算机严格验证。Mathlib（Mathematics Library）是Lean社区维护的核心数学库，目前已包含超过100万行代码和数十万条经过机器验证的数学定理，覆盖从基础代数到高级分析的广泛领域。与普通编程语言的代码库不同，Mathlib中每一条定理的证明都经过类型检查器的机械验证，这使得它成为迄今为止人类最大规模的经过严格验证的数学知识库。

Riemann-Stieltjes积分是经典Riemann积分的推广，由荷兰数学家Thomas Joannes Stieltjes于1894年引入。它将积分∫f dg中的积分测度从简单的dx推广为任意有界变差函数g的增量，在解析数论（如Abel求和公式）、概率论（随机过程的期望计算）和泛函分析中有广泛应用。Mathlib已经包含Lebesgue积分和一种非常通用的箱积分（box integral），但尚未将其特化为Riemann-Stieltjes积分。这一积分在解析数论中有重要应用——需要对有界变差函数或分段连续函数进行积分，而Mathlib现有的Stieltjes测度构造仅处理非负测度，无法直接处理复值函数的积分。

说个细节，Mathlib的设计哲学是"Bourbaki风格"——在最大程度的一般性上定义概念，然后再特化到常见用例，而非按照教学效率从具体到抽象逐步推广。Nicolas Bourbaki是一个法国数学家集体笔名，20世纪中期以极度抽象和公理化的方式重写了现代数学基础。Bourbaki风格强调从最一般的结构出发定义概念，再逐步特化到具体情形，与教学中常用的从具体到抽象的路径相反。Mathlib继承了这一哲学，这使得库中的定理具有最大的复用性，但也增加了入门贡献者的学习曲线——这意味着代码从一开始就在非常抽象的层面上工作。

Mathlib的严格风格指南：AI审查的用武之地

风格要求之严苛

Mathlib拥有极其详尽的代码风格指南，涵盖变量命名、行宽限制、输入结构、文档字符串格式、空白处理等方方面面。此外还有一套完全独立的命名指南，规定了数十万条引理的统一命名规范。

陶哲轩分享了自己的亲身经历：两周前他首次向Mathlib提交了约300行代码，结果收到了数百条审查意见，其中大量是风格合规性问题。这种情况对于非资深贡献者来说几乎不可避免。

Claude Code的红队工作流

陶哲轩为Claude Code开发了一套审计技能（skill），具体做法是：

1. 将Mathlib的网页版风格指南转化为Markdown文件，提取出可执行的检查项
2. 创建自动化扫描脚本，检查空格、空行、列宽等机械性问题
3. 让Claude逐段审查代码，提出合规性建议和优化方案

在演示中，Claude发现了多种问题：

• simp only at the goal中的冗余参数（simp only默认作用于目标）
• 双空行应改为单空行
• simp后跟exact可以合并为单个exact语句
• 保留字冲突（def是Lean的保留字，应使用_def替代）

实战演示：从代码审查到自动重构

机械性修复

Claude首先执行自动化扫描，处理空白、格式等机械性问题。这些修改虽然不"激动人心"，但陶哲轩认为这正是AI的理想用例："我不想把时间花在检查空白要求上，让Claude在后台处理这些，而我专注于解决数学问题，这是很好的分工。"

中等难度的重构：隐式参数优化

更有趣的是，Claude提出了一个实质性的重构建议：将某些引理中的显式参数（B、F、G）改为隐式参数。在Lean等依赖类型语言中，参数可以声明为显式（用圆括号）或隐式（用花括号或方括号）。隐式参数由类型检查器根据上下文自动推断，无需调用者手动提供，这大幅简化了定理的使用方式。将参数从显式改为隐式是Mathlib代码审查中的常见优化，能显著提升代码的可读性和易用性，但需要确保类型推断在所有使用场景中都能成功。在大多数使用场景中，这些参数可以从上下文推断出来，无需每次显式指定。

这个重构过程展示了AI辅助的典型工作流：

1. Claude修改了参数声明（从圆括号改为花括号）
2. 这导致多个文件出现编译错误
3. Claude通过grep查找所有受影响的位置
4. 逐一修复，删除不再需要的显式参数
5. 在某些Lean无法推断参数的地方，重新添加显式标注

重构过程中出现了一个意外收获：由于参数变为隐式后提供了更多上下文，Claude发现了一个更简洁的证明——原来的三行证明被压缩为更短的版本。

知识积累机制

Claude的审计技能文件底部有一个"gotchas"（陷阱）记录区。每当Claude在某处犯错（如忘记指定某些输入），它会记录下来，避免未来重复犯同样的错误。陶哲轩期望随着持续使用，这个工具会变得越来越高效。

局限性与人机协作的边界

陶哲轩也坦诚展示了Claude Code在数学形式化中的局限：

• 复杂数学证明仍需人工：例如证明"两个子区间上可积则大区间上也可积"这一引理，他明确表示不会让Claude尝试，因为"它要么失败，要么给出一个非常丑陋的证明，需要花大量时间重构