Understanding Analysis in Lean 4

This repository contains Lean 4 formalizations of proofs and exercises from Stephen Abbott's "Understanding Analysis" textbook. This project serves as both a learning tool for real analysis and an opportunity to practice formal mathematics in Lean 4.

Project Structure

• LeanUA/Chapter01/ - The Real Numbers
• LeanUA/Chapter02/ - Sequences and Series
• LeanUA/Chapter03/ - Basic Topology of R
• LeanUA/Chapter04/ - Functional Limits and Continuity
• LeanUA/Chapter05/ - The Derivative
• LeanUA/Chapter06/ - Sequences and Series of Functions
• LeanUA/Chapter07/ - The Riemann Integral
• LeanUA/Chapter08/ - Additional Topics
• LeanUA/Chapter09/ - Epilogue

Getting Started

Prerequisites

• Lean 4 (installed via elan)
• VS Code with the Lean 4 extension

Setup

1. Clone this repository:

   git clone <your-repo-url>
   cd lean_ua

2. Build the project:

   lake exe cache get
   lake build

Usage

Each chapter directory contains:

• Definitions and theorems from the corresponding textbook chapter
• Formalized proofs of key results
• Solutions to selected exercises
• Additional lemmas and helper functions

Learning Resources

• Lean 4 Manual
• Mathematics in Lean
• Natural Number Game
• Mathlib Documentation

Contributing

Feel free to:

• Add new proofs and exercises
• Improve existing formalizations
• Fix bugs or typos
• Enhance documentation

About Understanding Analysis

"Understanding Analysis" by Stephen Abbott is an excellent undergraduate textbook that provides a rigorous yet accessible introduction to real analysis. This formalization project aims to:

1. Deepen understanding of the mathematical concepts
2. Practice formal proof techniques in Lean 4
3. Create a reference implementation for students learning analysis
4. Demonstrate the power of computer-assisted proof verification

License

This project is licensed under the MIT License - see the LICENSE file for details.