Golfing and stylistically aligning a proof using Claude Code | Another Certified Hood Classic by Terrance Tao and Claude

TL;DR: 陶哲轩演示了如何使用 Claude Code 作为“红队”工具，帮助将手写的 Lean 代码风格对齐 Mathlib 官方风格指南，并以 Riemann–Stieltjes 积分的形式化项目为例。 ## 蓝队任务与红队任务 在数学形式化工作中，陶哲轩区分了两种任务： - **蓝队任务**：创造新内容，例如编写 Lean 证明或代码。这是工作中比较“光鲜”的部分，人们更喜欢做创造者而非验证者。 - **红队任务**：验证蓝队生成的内容是否正确，是否符合要求。这通常被认为更繁琐但必要。 对于 Lean 代码，蓝队任务可以借助 AI 工具（如 Claude Code）来生成，只要红队能力（如 Lean 的类型检查器）能跟上。类型检查器能立即检测代码是否通过类型检查，这使 AI 在拥有强验证的蓝队任务中相对安全。 但陶哲轩认为，AI 更适合做红队任务：人类生成内容，AI 检查内容的正确性、风格准确性或是否符合指定指导。如果不符合，AI 提出修改建议，但人类需保持警惕并监督修改。 ## Riemann–Stieltjes 积分的形式化项目 这个项目源自布朗大学 Zermin 举办的“分析形式化研讨会”。研讨会包含讲座和分组工作。每组选择一个目前缺失于 Mathlib 的分析主题，目标是生成达到 Mathlib 质量标准的代码，以便提交审核。 所选主题是 **Riemann–Stieltjes 积分**。 - Mathlib 已有 Lebesgue 积分和一种非常一般的“box 积分”（适用于任意维度的黎曼积分类，包含 Henstock 积分等）。 - 但这个一般积分尚未特化为 Riemann–Stieltjes 积分。 - Riemann–Stieltjes 积分在解析数论等应用中有用，允许对有界变差函数或分段连续函数积分。 - 目前 Mathlib 的测度构造仅处理非负测度，只能针对单调函数积分，而数论中常需要复值函数积分，复测度尚未在 Mathlib 中。 因此团队决定生成 Stieltjes 积分。已有数千行代码，定义了谓词 `has_stieltjes_integral`，基于 box 积分的 `has_integral`。Stieltjes 积分记为 `∫ f dg`（带一个 `B`，因为 f 和 g 可以是向量值）。Mathlib 的惯例是以最大泛化程度定义所有术语，再特化为常见用例——Bourbaki 式的阐述方式，注重基础效率而非教学效率。 ## Mathlib 风格指南 Mathlib 有严格的官方库风格指南，非常详细：如何命名变量、行长、输入结构、文档字符串样式、定理结构、空格、空白、命名约定等。还有独立指南专门针对命题和定义命名。 风格指南初看像“CI soup”——华丽而巴洛克，但实际上非常有用。Mathlib 有数十万条引理，统一风格使你能通过名字快速理解引理内容（例如 `le_of_forall_lt`）。几乎不可能在第一次尝试时完全符合指南，尤其是对于非资深贡献者。陶哲轩两周前提交了第一次 Mathlib 贡献（约300行代码），收到了数百条评论，很多是关于风格不符合指南。 目前正努力自动化部分检查（如列宽限制），已有一些 linter 工具，但主要仍是人工任务。这类红队任务正是 AI 工具当前能帮忙的地方。 ## 使用 Claude Code 进行风格对齐 陶哲轩演示了使用 Claude Code 开发一个技能：审计文件是否符合 Mathlib 风格。他让 Claude 将 Mathlib 风格指南转换成一个 markdown 文件，包含具体可操作项（如检查间距是否正确等），然后运行扫描。 找到了一些小问题： - 一个方法叫 `integral.deaf`，但 `deaf` 是 Lean 中的保留字。经与 Mathlib 核查，首选名称是 `_deaf`，于是做了修改。 - 其他机械性问题：第78行的 `simp` 在目标上默认工作，可以删除冗余；双空行应改为单空行；等等。 Claude 还注意到一个模式：代码先定义从 a 到 b 的积分（递增积分），再扩展为可反向积分（通过取反定义）。许多定理需要证明两次（正向和双向），Claude 询问是否应创建抽象引理或策略，但最终建议保持现状。 有些地方使用了 `convert` 策略，虽然强大但 Mathlib 不推荐，因为更简单的策略更稳定。陶哲轩尝试过更简单策略但困难，Claude 也建议不改动。 整体上，这段代码已被大量修改过（最初是通过计算机生成的大量重复代码：加法引理、标量乘法引理、取反引理等）。陶哲轩先手工写了前几个，让 Claude 用同样风格生成了后续40–50个，Claude 尽职地完成了。 ## 结论 通过这个案例，陶哲轩展示了 AI（Claude Code）作为红队工具的价值：不是替代人类创造，而是帮助人类确保代码符合库的严格风格标准，从而加速形式化工作并提高提交通过率。 --- Source: [https://youtu.be/l3SCK6V-BFw?si=GxbP0Y_q0Qi66-5w](https://youtu.be/l3SCK6V-BFw?si=GxbP0Y_q0Qi66-5w)