Terence Tao Uses Claude Code for Math Proof Review: Red Team Tasks More Valuable Than Blue Team

Overview: A New Role for AI in Mathematical Formalization

Mathematician Terence Tao recently released a demo video showcasing how he uses Claude Code to assist with mathematical formalization work. Unlike previous uses of AI to generate Lean proof code ("blue team tasks"), this time he focused on demonstrating AI's application in "red team tasks" — where humans write the code and AI handles review, validation, and optimization.

The concepts of Red Team and Blue Team originate from military and cybersecurity domains: red teams simulate attacks and find vulnerabilities; blue teams defend and verify. In AI safety, red teaming has become a standard method for evaluating large language model safety. Tao brings this framework to mathematical formalization, using "red team" to refer to verification and review work, and "blue team" to refer to creative generation work — an analogy that intuitively reveals the fundamental differences between these two types of tasks in terms of risk profiles and required capabilities.

Tao explicitly distinguishes between the two: Blue team tasks are creative work, such as writing new Lean proofs; Red team tasks are verification and checking work, ensuring code correctness and style compliance. He argues that AI's value in red team tasks may even exceed that of blue team tasks, because this type of tedious but necessary work is precisely where AI shines.

Background: Formalizing the Riemann-Stieltjes Integral in Mathlib

This work originated from an analysis formalization workshop held last week at the ISM at Brown University. Participants split into groups and chose missing analysis topics in Lean's central mathematics library (Mathlib) to formalize. Tao's group chose the Riemann-Stieltjes integral.

About Lean and Mathlib: Lean is an interactive theorem prover and functional programming language developed by Leonardo de Moura at Microsoft Research, with the core design goal of enabling computer-verified mathematical proofs. Mathlib (Mathematics Library) is the core math library maintained by the Lean community, currently containing over 1 million lines of code and hundreds of thousands of machine-verified mathematical theorems, covering topics from basic algebra to advanced analysis. Unlike codebases in ordinary programming languages, every theorem proof in Mathlib is mechanically verified by a type checker, making it the largest rigorously verified mathematical knowledge base ever created by humanity.

The Riemann-Stieltjes integral is a generalization of the classical Riemann integral, introduced by Dutch mathematician Thomas Joannes Stieltjes in 1894. It generalizes the integration measure in ∫f dg from simple dx to increments of any function g of bounded variation, with broad applications in analytic number theory (such as Abel's summation formula), probability theory (expectation calculations for stochastic processes), and functional analysis. Mathlib already contains the Lebesgue integral and a very general box integral, but has not yet specialized these into the Riemann-Stieltjes integral. This integral has important applications in analytic number theory — requiring integration against functions of bounded variation or piecewise continuous functions — while Mathlib's existing Stieltjes measure construction only handles non-negative measures and cannot directly handle integration of complex-valued functions.

As a side note, Mathlib's design philosophy is "Bourbaki-style" — defining concepts at the maximum level of generality, then specializing to common use cases, rather than gradually generalizing from concrete to abstract as in pedagogical approaches. Nicolas Bourbaki is a collective pseudonym for a group of French mathematicians who, in the mid-20th century, rewrote the foundations of modern mathematics in an extremely abstract and axiomatic manner. The Bourbaki style emphasizes defining concepts from the most general structures and then progressively specializing to concrete cases — the opposite of the concrete-to-abstract path common in teaching. Mathlib inherits this philosophy, which gives theorems in the library maximum reusability but also increases the learning curve for new contributors — meaning the code works at a very abstract level from the start.

Mathlib's Strict Style Guide: Where AI Review Excels

The Rigor of Style Requirements

Mathlib has an extremely detailed code style guide covering variable naming, line width limits, input structure, docstring format, whitespace handling, and much more. There's also a completely separate naming guide that specifies uniform naming conventions for hundreds of thousands of lemmas.

Tao shared his own experience: two weeks ago he submitted approximately 300 lines of code to Mathlib for the first time and received hundreds of review comments, many of which were style compliance issues. This situation is almost unavoidable for non-veteran contributors.

Claude Code's Red Team Workflow

Tao developed a set of auditing skills for Claude Code, with the specific approach being:

1. Converting Mathlib's web-based style guide into Markdown files, extracting actionable check items
2. Creating automated scanning scripts to check spacing, blank lines, column width, and other mechanical issues
3. Having Claude review code section by section, offering compliance suggestions and optimization proposals

In the demo, Claude identified multiple issues:

• Redundant arguments in simp only at the goal (simp only targets the goal by default)
• Double blank lines that should be single blank lines
• simp followed by exact that can be merged into a single exact statement
• Reserved word conflicts (def is a Lean reserved word; _def should be used instead)

Live Demo: From Code Review to Automated Refactoring

Mechanical Fixes

Claude first executes automated scans, handling whitespace, formatting, and other mechanical issues. While these changes aren't "exciting," Tao considers this an ideal AI use case: "I don't want to spend my time checking whitespace requirements. Let Claude handle these in the background while I focus on solving math problems — that's a good division of labor."

Medium-Difficulty Refactoring: Implicit Parameter Optimization

More interesting was Claude's suggestion for a substantive refactoring: changing certain explicit parameters (B, F, G) in some lemmas to implicit parameters. In dependently typed languages like Lean, parameters can be declared as explicit (using parentheses) or implicit (using curly braces or square brackets). Implicit parameters are automatically inferred by the type checker from context, without requiring the caller to provide them manually, which greatly simplifies how theorems are used. Changing parameters from explicit to implicit is a common optimization in Mathlib code review that significantly improves code readability and usability, but requires ensuring that type inference succeeds in all usage scenarios. In most use cases, these parameters can be inferred from context without needing to be explicitly specified each time.

This refactoring process demonstrates a typical AI-assisted workflow:

1. Claude modified the parameter declarations (from parentheses to curly braces)
2. This caused compilation errors in multiple files
3. Claude used grep to find all affected locations
4. Fixed them one by one, removing explicit parameters that were no longer needed
5. In places where Lean couldn't infer the parameters, re-added explicit annotations

An unexpected bonus emerged during the refactoring: since the implicit parameters provided more context, Claude discovered a more concise proof — the original three-line proof was compressed into a shorter version.

Knowledge Accumulation Mechanism

At the bottom of Claude's auditing skill file, there's a "gotchas" recording section. Whenever Claude makes a mistake (such as forgetting to specify certain inputs), it records the error to avoid repeating the same mistake in the future. Tao expects that with continued use, this tool will become increasingly efficient.

Limitations and the Boundaries of Human-AI Collaboration

Tao also candidly demonstrated Claude Code's limitations in mathematical formalization:

• Complex mathematical proofs still require human work: For example, proving the lemma "integrability on two subintervals implies integrability on the larger interval" — he explicitly stated he wouldn't ask Claude to attempt it, because "it would either fail or produce a very ugly proof that would take a lot of time to refactor."