Formalization of Real Analysis by Jay Cummings

Welcome to the real-analysis repository, a Lean4 formalization of Real Analysis based on the book by Jay Cummings.

About the Book and Author

For more information about the book and its author, visit Longform Math.

Author's Permission

We gratefully acknowledge Jay Cummings for granting permission to formalize the exercises from his book.

Chapters

The content is organized into the following chapters:

1. The Reals
2. Cardinality
3. Sequences
4. Series
5. The Topology of R
6. Continuity
7. Differentiation
8. Integration
9. Sequences and Series of Functions

---

Feel free to reach out if you have any questions or suggestions. Contributions are welcome!

---