// the find
teorth/analysis
A Lean companion to Analysis I
A section-by-section Lean 4 formalization of Terence Tao's 'Analysis I' textbook, written by Tao himself. It's for people learning Lean/Mathlib who already know real analysis and want to see the proofs made fully rigorous, or for Lean users who want a guided on-ramp into Mathlib's number and real-analysis hierarchy.
The pedagogical structure is the whole point and it's done well: definitions start fully self-contained (e.g. a from-scratch inductive ℕ in Chapter 2) and are deliberately migrated to Mathlib's versions chapter by chapter, with epilogues proving the isomorphism — so you see exactly where and why the 'real' Mathlib definitions diverge from the textbook ones. Every section has a generated docs page, a Verso page, and a direct link to source, plus CI (build_book.yml) that keeps the whole thing compiling as Mathlib moves. The scope creep beyond the textbook (a measure theory formalization, Erdos problem solutions, a units-of-measurement system) is a genuine bonus, not padding — it shows the repo is a live research notebook, not a one-off course artifact.
Exercises are deliberately left as `sorry`, and solutions aren't provided in the repo — if you're using this to check your own proofs, you're on your own or trawling the linked Zulip thread. The README is upfront that the code is 'not optimized for efficiency' and 'may deviate from idiomatic Lean usage,' so don't copy patterns from here into production Lean/Mathlib code. Bumping Lean/Mathlib versions is explicitly called out as a manual, deprecated-method workaround in the README rather than something lakefile tooling handles cleanly, which is a bit of a wart for a repo this prominent. And because it tracks Mathlib's HEAD, older chapters can quietly need touch-ups whenever upstream renames or restructures something.