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

**TL;DR:** Terence Tao demonstrates how to use Claude Code as a "red team" tool to help align hand-written Lean code with the official Mathlib style guide, using the formalization of the Riemann–Stieltjes integral as an example. ## Blue Team Tasks and Red Team Tasks In mathematical formalization work, Terence Tao distinguishes two types of tasks: - **Blue team tasks**: creating new content, such as writing Lean proofs or code. This is the more "glamorous" part of the work — people prefer to be creators rather than verifiers. - **Red team tasks**: verifying that the blue team's output is correct and meets requirements. This is often considered more tedious but necessary. For Lean code, blue team tasks can be assisted by AI tools (like Claude Code) as long as the red team capability (e.g., Lean's type checker) keeps up. The type checker immediately detects whether the code passes type checking, which makes AI relatively safe in blue team tasks that have strong verification. But Tao believes AI is better suited for red team tasks: humans generate content, AI checks it for correctness, style accuracy, or compliance with specified guidelines. If something doesn't match, AI suggests modifications, but humans must remain vigilant and oversee the changes. ## The Riemann–Stieltjes Integral Formalization Project This project originated from the "Analysis Formalization Workshop" held by Zermin at Brown University. The workshop included lectures and group work. Each group chose an analysis topic currently missing from Mathlib, aiming to produce code that meets Mathlib quality standards for submission. The chosen topic was the **Riemann–Stieltjes integral**. - Mathlib already has the Lebesgue integral and a very general "box integral" (applicable to any-dimensional Riemann-type integrals, including Henstock integrals, etc.). - But this general integral has not yet been specialized to the Riemann–Stieltjes integral. - The Riemann–Stieltjes integral is useful in applications such as analytic number theory, allowing integration with respect to functions of bounded variation or piecewise continuous functions. - Currently, Mathlib's measure construction only handles nonnegative measures, so integration can only be performed against monotone functions. In number theory, one often needs to integrate complex-valued functions, and complex measures are not yet available in Mathlib. Thus the team decided to produce the Stieltjes integral. Thousands of lines of code already exist, defining a predicate `has_stieltjes_integral` based on the `has_integral` of the box integral. The Stieltjes integral is denoted `∫ f dg` (with a `B`, because `f` and `g` can be vector-valued). Mathlib follows a convention of defining all terms at the maximum level of generality and then specializing to common use cases — a Bourbaki-style exposition that prioritizes structural efficiency over pedagogical efficiency. ## The Mathlib Style Guide Mathlib has a strict official library style guide, very detailed: how to name variables, line length, indentation structure, docstring style, theorem structure, spacing, whitespace, naming conventions, and more. There is a separate guide specifically for naming propositions and definitions. At first glance, the style guide looks like "CI soup" — ornate and baroque — but it is actually highly useful. Mathlib has hundreds of thousands of lemmas; a consistent style allows you to quickly understand a lemma's content from its name (e.g., `le_of_forall_lt`). It is almost impossible to conform to the guide on the first attempt, especially for non-seasoned contributors. Tao submitted his first Mathlib contribution (about 300 lines of code) two weeks ago and received hundreds of comments, many about style not conforming to the guide. Efforts are underway to automate some checks (e.g., line width limits), and some linter tools exist, but the bulk is still a manual task. This kind of red team task is exactly where AI tools can currently help. ## Using Claude Code for Style Alignment Tao demonstrated using Claude Code to develop a skill: auditing a file for compliance with Mathlib style. He asked Claude to convert the Mathlib style guide into a markdown file with concrete actionable items (e.g., check spacing correctness, etc.), and then run a scan. A few minor issues were found: - A method called `integral.deaf`, but `deaf` is a reserved word in Lean. After checking with Mathlib, the preferred name is `_deaf`, so it was changed. - Other mechanical issues: the `simp` at line 78 works by default on the goal and could be removed as redundant; double blank lines should be changed to single blank lines; etc. Claude also noticed a pattern: the code first defines the integral from a to b (increasing integral), then extends it to allow reverse integration (by defining via negation). Many theorems need to be proved twice (forward and bidirectional). Claude asked whether abstract lemmas or a tactic should be created, but ultimately suggested keeping it as is. In some places, the `convert` tactic was used; though powerful, Mathlib does not recommend it because simpler tactics are more stable. Tao tried simpler tactics but found it difficult; Claude also suggested not to change it. Overall, this code has been heavily modified (originally a large amount of repetitive code generated by a computer: addition lemmas, scalar multiplication lemmas, negation lemmas, etc.). Tao manually wrote the first few, then asked Claude to generate the next 40–50 using the same style, and Claude dutifully did so. ## Conclusion Through this case, Tao demonstrated the value of AI (Claude Code) as a red team tool: not to replace human creation, but to help humans ensure that code adheres to the library's strict style standards, thereby accelerating formalization work and improving submission acceptance rates. --- Source: https://youtu.be/l3SCK6V-BFw?si=GxbP0Y_q0Qi66-5w