Reservoir

Partial Lean formalization of Analysis I

The files in this directory contain a formalization of selected portions of my text Analysis I into Lean. The formalization is intended to be as faithful a paraphrasing as possible to the original text, while also showcasing Lean's features and syntax. In particular, the formalization is not optimized for efficiency, and in some cases may deviate from idiomatic Lean usage.

Portions of the text that were left as exercises to the reader are rendered in this translation as sorrys. Readers are welcome to fork the repository here to try their hand at these exercises, but I do not intend to place solutions in this repository directly.

While the arrangement of definitions, theorems, and proofs here are closely paraphrasing the textbook, I am refraining from directly quoting material from the textbook, instead providing references to the original text where appropriate. As such, this formalization should be viewed as an annotated companion to the primary text, rather than a replacement for it.

Much of the material in this text is duplicated in Lean's standard math library Mathlib, though with slightly different definitions. To reconcile these discrepancies, this formalization will gradually transition from the textbook-provided definitions to the Mathlib-provided definitions as one progresses further into the text, thus sacrificing the self-containedness of the formalization in favor of compatibility with Mathlib. For instance, Chapter 2 develops a theory of the natural numbers independent of Mathlib, but all subsequent chapters will use the Mathlib natural numbers instead. (An epilogue to Chapter 2 is provided to show that the two notions of the natural numbers are isomorphic.) As such, this formalization can also be used as an introduction to various portions of Mathlib.

In order to align the formalization with Mathlib conventions, a small number of technical changes have been made to some of the definitions as compared with the textbook version. Most notably:

• Sequences are indexed to start from zero rather than from one, as Mathlib has much more support for the 0-based natural numbers ℕ than the 1-based natural numbers.
• Many operations that are left undefined in the text, such as division by zero, or taking the formal limit of a non-Cauchy sequence, are instead assigned a "junk" value (e.g., 0) to make the operation totally defined. This is because Lean has better support for total functions than partial functions (indiscriminate use of the latter can lead into "dependent type hell" in which even very basic manipulations require quite subtle and delicate proofs). See for instance this blog post by Kevin Buzzard for more discussion.
• The Chapter 2 natural numbers are constructed by an inductive type, rather than via a purely axiomatic approach. However, the Peano Axioms are formalized in the epilogue to this chapter.

Sections

• Chapter 1: Introduction (possible future expansion)
• Chapter 2: Starting at the beginning: the natural numbers
  • Section 2.1: The Peano axioms (Verso page) (Documentation) (Lean source)
  • Section 2.2: Addition (Verso page) (Documentation) (Lean source)
  • Section 2.3: Multiplication (Verso page) (Documentation) (Lean source)
  • Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers (Verso page) (Documentation) (Lean source)
• Chapter 3: Set theory
  • Section 3.1: Fundamentals (Verso page) (Documentation) (Lean source)
  • Section 3.2: Russell's paradox (Verso page) (Documentation) (Lean source)
  • Section 3.3: Functions (Verso page) (Documentation) (Lean source)
  • Section 3.4: Images and inverse images (Verso page) (Documentation) (Lean source)
  • Section 3.5: Cartesian products (Verso page) (Documentation) (Lean source)
  • Section 3.6: Cardinality of sets (Verso page) (Documentation) (Lean source)
• Chapter 4: Integers and rationals
  • Section 4.1: The integers (Verso page) (Documentation) (Lean source)
  • Section 4.2: The rationals (Verso page) (Documentation) (Lean source)
  • Section 4.3: Absolute value and exponentiation (Verso page) (Documentation) (Lean source)
  • Section 4.4: Gaps in the rational numbers (Verso page) (Documentation) (Lean source)
• Chapter 5: The Real numbers
  • Section 5.1: Cauchy sequences of rationals (Verso page) (Documentation) (Lean source)
  • Section 5.2: Equivalent Cauchy sequences (Verso page) (Documentation) (Lean source)
  • Section 5.3: Construction of the real numbers (Verso page) (Documentation) (Lean source)
  • Section 5.4: Ordering the reals (Verso page) (Documentation) (Lean source)
  • Section 5.5: The least upper bound property (Verso page) (Documentation) (Lean source)
  • Section 5.6: Real exponentiation, part I (possible future expansion)
  • Chapter 5 epilogue: Isomorphism with the Mathlib real numbers (Verso page) (Documentation) (Lean source)
• Chapter 6: Limits of sequences
  • Section 6.1: Convergence and limit laws (Verso page) (Documentation) (Lean source)
  • Section 6.2: The extended real number system (Verso page) (Documentation) (Lean source)
  • Section 6.3: Suprema and Infima of sequences (Verso page) (Documentation) (Lean source)
  • Section 6.4: Limsup, Liminf, and limit points (Verso page) (Documentation) (Lean source)
  • Section 6.5: Some standard limits (Verso page) (Documentation) (Lean source)
  • Section 6.6: Subsequences (Verso page) (Documentation) (Lean source)
  • Section 6.7: Real exponentiation, part II (possible future expansion)
  • Chapter 6 epilogue: Connections with Mathlib limits (Verso page) (Documentation) (Lean source)
• Chapter 7: Series
  • Section 7.1: Finite series (Verso page) (Documentation) (Lean source)
  • Section 7.2: Infinite series (Verso page) (Documentation) (Lean source)
  • Section 7.3: Sums of non-negative numbers (Verso page) (Documentation) (Lean source)
  • Section 7.4: Rearrangement of series (Verso page) (Documentation) (Lean source)
  • Section 7.5: The root and ratio tests (Verso page) (Documentation) (Lean source)
• Chapter 8: Infinite sets (possible future expansion)
• Chapter 9: Continuous functions on ℝ
  • Section 9.1: Subsets of the real line (Verso page) (Documentation) (Lean source)
  • Section 9.2: The algebra of real-valued functions (Verso page) (Documentation) (Lean source)
  • Section 9.3: Limiting values of functions (Verso page) (Documentation) (Lean source)
  • Section 9.4: Continuous functions (Verso page) (Documentation) (Lean source)
  • Section 9.5: Left and right limits (Verso page) (Documentation) (Lean source)
  • Section 9.6: The maximum principle (Verso page) (Documentation) (Lean source)
  • Section 9.7: The intermediate value theorem (Verso page) (Documentation) (Lean source)
  • Section 9.8: Monotonic functions (Verso page) (Documentation) (Lean source)
  • Section 9.9: Uniform continuity (Verso page) (Documentation) (Lean source)
  • Section 9.10: Limits at infinity (Verso page) (Documentation) (Lean source)
• Chapter 10: Differentiation of functions
  • Section 10.1: Basic definitions (Verso page) (Documentation) (Lean source)
  • Section 10.2: Local maxima, local minima, and derivatives (Verso page) (Documentation) (Lean source)
  • Section 10.3: Monotone functions and derivatives (Verso page) (Documentation) (Lean source)
  • Section 10.4: Inverse functions and derivatives (Verso page) (Documentation) (Lean source)
  • Section 10.5: L'Hôpital's rule (Verso page) (Documentation) (Lean source)
• Chapter 11: The Riemann integral
  • Section 11.1: Partitions (planned)
  • Section 11.2: Piecewise constant functions (planned)
  • Section 11.3: Upper and lower Riemann integrals (planned)
  • Section 11.4: Basic properties of the Riemann integral (planned)
  • Section 11.5: Riemann integrability of continuous functions (planned)
  • Section 11.6: Riemann integrability of monotone functions (planned)
  • Section 11.7: A non-Riemann integrable function (planned)
  • Section 11.8: The Riemann-Stieltjes integral (planned)
  • Section 11.9: The two fundamental theorems of calculus (planned)
  • Section 11.10: Consequences of the fundamental theorem of calculus (planned)
• Appendix A: The basics of mathematical logic
  • A.1: Mathematical statements (Verso page) (Documentation) (Lean source)
  • A.2: Implication (Verso page) (Documentation) (Lean source)
  • A.3: The structure of proofs (Verso page) (Documentation) (Lean source)
  • A.4: Variables and quantifiers (Verso page) (Documentation) (Lean source)
  • A.5: Nested quantifiers (Verso page) (Documentation) (Lean source)
  • A.6: Some examples of proofs and quantifiers (Verso page) (Documentation) (Lean source)
  • A.7: Equality (Verso page) (Documentation) (Lean source)
• Appendix B: The decimal system (possible future expansion)

Other resources

• Web page for this project
  • Documentation
• Web page for the book
  • Springer edition
• Blog post announcing this project, Terence Tao, May 31 2025.
• Lean Zulip discussion about this project
• Notes for contributors

General Lean resources

• The Lean community
  • Lean4 web playground
  • How to run a project in Lean locally
  • The Lean community Zulip chat
  • Learning Lean4
    • The natural number game
    • Mathematics in Lean - Lean textbook by Jeremy Avigad and Patrick Massot
• Mathlib documentation
  • Moogle - semantic search engine for Mathlib
  • Loogle - expression matching search engine for Mathlib
  • LeanSearch - Natural language search engine for Mathlib
  • List of Mathlib tactics
• Lean extensions:
  • Canonical
  • Duper
  • LeanCopilot
• Common Lean pitfalls
• Lean4 questions in Proof Stack Exchange
• The mechanics of proof - introductory Lean textbook by Heather Macbeth
• My Youtube channel has some demonstrations of various Lean formalization, using a variety of tools.
• A broader list of AI and formal mathematics resources.

More resource suggestions welcome!

Building

Building the project

To build this project after installing Lean and cloning this repository, follow these steps:

% cd analysis/
% cd Analysis/
% lake exe cache get
% lake build

Building the project's web page

To build the project's web page after installing Lean and cloning this repository, follow these steps:

% cd analysis/
% cd Analysis/
% lake exe cache get
% lake -R -Kenv=dev build Analysis:docs
% lake build
% cd ../
% cd book/
% lake exe analysis-book
% cd ../

After this, book/_site/ contains the project's web page. This can be served as a webpage by executing python3 serve.py