MAT3253 Complex Variables🔗

Lean proof of selected theorems in the notes for the course MAT3253 Complex Variables.

The program compiles with Mathlib 4.29.

Inspired by Terence Tao’s Lean Companion to Analysis I, the goal of this repository is to provide faithful Lean translations of proofs from the textbook, following the structure and reasoning of the original arguments as closely as possible. While many of these results already appear in Mathlib, the library versions are often intentionally concise. In contrast, the proofs here aim to be pedagogically transparent, mirroring the step‑by‑step style of the textbook.

Lean is designed to be proof‑irrelevant: two proofs of the same proposition are considered definitionally interchangeable. Thus, both the detailed textbook‑style proofs and the shorter Mathlib proofs are equally valid in Lean. Nevertheless, the expanded versions can be more helpful for learners who want to see the intermediate reasoning, while the Mathlib versions are ideal for reuse in later developments.

---

Funding Acknowledgment

This project is partially funded by CUHK(SZ) CLEAR Teaching Innovation Grant (2024), "Enhancement of mathematical learning using the LEAN computer proof assistant".

---

Contributors

Parts of the formalization were developed with assistance from Harmonic Aristotle, ChatGPT 5.5, and Gemini 3.1.