A Lean companion to Analysis I: what it formalizes, what it skips, and where it diverges

What the project actually is

This repository is a formalization of Terence Tao's Analysis I textbook into the Lean theorem prover. It is not a standalone text and it is not a complete translation. The README is explicit: the formalization is intended as a faithful paraphrasing of the original text, with references provided instead of direct quotes. It is an annotated companion. The target audience is someone who is already reading the book and wants to see the definitions and proofs in a machine-checked form, or someone who wants to learn Mathlib by seeing how a standard textbook gets encoded. The project does not aim to be idiomatic Lean or efficient. It prioritizes closeness to the textbook over style. That is a deliberate choice, and it shows in the code, as the README admits deviations from idiomatic usage.

The chapter-by-chapter structure and the transition to Mathlib

The repository is organized by textbook sections. Chapter 1 is not formalized at all. Chapter 2 starts with a self-contained construction of the natural numbers, built as an inductive type, and it deliberately avoids Mathlib's natural numbers. Then the epilogue to Chapter 2 proves an isomorphism between that custom type and Mathlib's `ℕ`. From Chapter 3 onward, the formalization uses Mathlib's natural numbers. The README gives a concrete example: sequences are indexed from zero instead of one, because Mathlib has more support for 0-based `ℕ`. This transition means the early chapters are self-contained, but later chapters depend on Mathlib's definitions and can be used as an introduction to Mathlib itself. The cost is that the formalization is not a single coherent theory; it is a bridge from a textbook presentation to a library.

How the formalization handles undefined operations

The textbook leaves some operations undefined, such as division by zero or the limit of a non-Cauchy sequence. Lean, as a total function language, cannot represent partial functions easily. The project assigns junk values, typically `0`, to make those operations total. The README cites Kevin Buzzard's blog post on division by zero in type theory to justify this. This is a pragmatic choice, but it changes the meaning of the statements. A theorem that says `x / 0 = 0` is not a theorem in the textbook; it is a theorem in Lean. Anyone reading the formalization must keep this in mind. The alternative, using partial functions, would lead to what the README calls 'dependent type hell', where even basic manipulations require delicate proofs. The trade-off is clear: total functions are easier to work with, but the formal statements are not always faithful to the informal ones.

The role of sorry and the unresolved exercises

The README states that portions of the text left as exercises are rendered as `sorry`. That is a Lean placeholder that allows the file to compile without a proof. The author explicitly says he does not intend to place solutions in the repository. This is a significant limitation. If you are using the repository to learn analysis, you will hit gaps exactly where the textbook asks you to work. If you are using it to verify the textbook's claims, you will not get a complete verification. The README invites readers to fork the repository and try the exercises themselves, which is a reasonable open-source approach, but it means the project is permanently incomplete by design. The presence of `sorry` also means that the formalization is not a fully verified proof of the book's theorems; it is a partial one.

Getting started: what you need to run it

The README does not include installation instructions, but the repository is a Lean project, and the source files are in the `Analysis` directory. The documentation is hosted at `https://teorth.github.io/analysis/`, with a Verso page and a generated HTML doc for each section. You can browse the Lean source directly on GitHub. To build the project locally, you would typically use `lake` (Lean's build tool) and `lake exe cache get` to fetch Mathlib, assuming the project has a `lakefile.toml` and a `lean-toolchain` file. The README does not specify these details, so you should check the repository root for the exact setup. The source files are named like `Section_2_1.lean`, `Section_2_2.lean`, and so on. The documentation pages give a rendered view of the proofs, which is useful if you do not want to install Lean. The project is Apache-2.0 licensed, which is permissive for forking and modification.

A genuine limitation: the risk of misleading faithfulness

The project's core value is also its core risk. Because it paraphrases the textbook closely, readers may assume that a theorem in Lean is exactly the same as the one in the book. The README lists specific deviations: 0-based indexing, junk values for undefined operations, and an inductive construction of the naturals instead of an axiomatic one. These are not cosmetic. A theorem about limits in the book may have a different statement in Lean because the limit is total and returns `0` for non-Cauchy sequences. This means you cannot blindly transfer a proof from the formalization back to the textbook. The project is a companion, not a replacement, and the README says so. If you are looking for a formalization that matches the book's definitions exactly, this will frustrate you. If you are looking for a way to see how a standard analysis text gets encoded in Lean, it is exactly right.

The alternative: using Mathlib directly

The obvious alternative to this repository is Mathlib itself. Mathlib already contains much of the material in Analysis I, with definitions that are more idiomatic and better integrated with the rest of the library. The README acknowledges this duplication. The difference in approach is that Mathlib is a general-purpose library, not a textbook companion. Its definitions are optimized for internal consistency and usability, not for matching a printed page. For example, Mathlib's natural numbers are the built-in `ℕ`, and its sequences are 0-based. If you want to learn analysis in Lean, you could read Mathlib's documentation and its theorem statements directly. But Mathlib is huge and not organized by textbook chapters. This repository provides a guided path through the book, with the transition to Mathlib built in. For a learner, that path is valuable. For a researcher who just needs a theorem, Mathlib is the better source.

Maintenance and upgrade cost

The repository is not archived, but the README does not mention any release schedule or versioning. The last push date is unknown, and no recent releases were retrieved. That is a risk. Lean and Mathlib evolve quickly, and a project that depends on Mathlib may break when Mathlib changes. The README's note that later chapters use Mathlib definitions means the project is tied to Mathlib's API. If Mathlib changes its definitions, the proofs in this repository may need updates. The author is Terry Tao, but the README does not state who maintains the repository or how often it is updated. The Apache-2.0 license allows anyone to fork and maintain it, but there is no guarantee of active maintenance. Before adopting it as a dependency, you should check the commit history and the current build status. The project is more of a living document than a stable library.

Editorial conclusion

If you are studying Analysis I and know enough Lean to read proofs, this repository is a valuable cross-reference: it shows how the textbook's definitions map to Lean, and where they intentionally diverge. If you want a complete, self-contained formalization of real analysis, or if you expect every exercise to be solved, this is not the right tool yet. Before using it, verify which sections are actually formalized (Chapter 1 is not, and later chapters may be incomplete), and check the current state of the `sorry`s, since the README states that exercise solutions are intentionally left out. The project is Apache-2.0, so you can fork it and try the exercises yourself, but do not expect the author to add solutions.

Official sources

1. Official documentation
2. Official README
3. Project repository