Formalization of "Analysis I" by Terence Tao

The goal of this project is to formalize the book "Analysis I" by Terence Tao, including the main text and the exercises. This is a work in progress. The formalization is done in Lean using the Mathlib library (currently version 4).

We acknowledge the use of AI tools to assist in the formalization process, notably GitHub Copilot.

Progress

(Updated on 2025-03-10)

Main text

Solutions to exercises

License

The project is licensed under the MIT License. See LICENSE for details.