Formalization & Proof Verification. MATH 153 is a gateway to modern mathematics: a mathematically sound framework for constructing and checking rigorous proofs. Over the semester, we bridge classical mathematical reasoning and interactive computer theorem proving using the Lean proof assistant, introducing students to an AI- and computer-assisted paradigm of modern mathematical research.
Course Information
- Instructor: Shen-Ning Tung (tung@math.nthu.edu.tw)
- Lecture Time: Wednesdays, periods 3–4 and Fridays, periods 5–6
- Office Hours: After class / by appointment
- Prerequisites: None. Students must bring a laptop to every class practice session capable of running VS Code and the Lean 4 toolchain.
- Target Audience: Lower-level undergraduate students and anyone eager to explore the formalization of mathematics. No prior university-level mathematical background or programming experience is required.
Course Description
To balance abstract mathematical concepts with hands-on technical proficiency, the course splits its contact hours evenly:
- Lectures (50%): Structural academic presentations detailing logical systems, deductive proof structures, and essential mathematical definitions.
- Exercises & Discussions (50%): Interactive, laboratory-style sessions. Students will actively write code, debug proofs in real time, and collaborate on solving logical tactics in class.
Learning Objectives
By the end of this course, students will be able to:
- Write mathematical proofs with absolute logical rigor.
- Read — dissect and programmatically verify mathematical proofs inside the Lean environment.
- Translate standard informal mathematical English into fully formalized Lean code.
Evaluation
| Assessment | Weight | Description |
|---|---|---|
| In-class Test & Practice | 100% | Weekly in-class computational problem sets. Students work out mathematical proofs manually, then translate and formally verify them using Lean. Spot checks will be conducted where selected students present and explain their interactive proof tactics to the class. |
| Oral Re-evaluation Exam | Optional | Reserved at the instructor’s discretion for individual students who exhibit insufficient evidence of learning progress or to resolve academic integrity discrepancies. |
Course Schedule
The curriculum is structured into four progressive phases, moving from basic computational proofs to advanced undergraduate mathematical structures: 13 content modules across 16 weeks, with three consolidation/buffer weeks built in so students have time to absorb material before moving on.
| Week | Module | Topic |
|---|---|---|
| 1 | 0 | Preface |
| 2 | 1 | Proofs by Calculation |
| 3 | 2 | Proofs with Structure |
| 4 | 3 | Parity, Divisibility & Number Theory |
| 5 | 4 | Proofs with Structure, II |
| 6 | — | Consolidation week — extended practice across Modules 0–4 |
| 7 | 5 | Logic |
| 8 | 6 | Induction |
| 9 | 7 | Functions |
| 10 | 8 | Sets |
| 11 | 9 | Relations |
| 12 | — | Consolidation week — extended practice across Modules 7–9 |
| 13 | 10 | Groups and Rings |
| 14 | 11 | Linear Algebra |
| 15 | 12 | Differential Calculus (elementary, single-variable scope) |
| 16 | — | Review / buffer week |
Course Phases
- Phase I — Foundations of Concrete Proofs (Modules 0–4): Setting up the Lean environment; rewriting and evaluating expressions; assumptions, goals, and step-by-step reasoning; formalizing parity, divisibility, and basic number theory; deepening tactical control with nested proof states.
- Phase II — Pure Logic & Metatheory (Modules 5–6): Propositional logic, quantifiers ($\forall, \exists$), conjunctions, and implications; the induction principle and proofs over natural numbers.
- Phase III — Classical Core Math (Modules 7–9): Functions (injectivity, surjectivity, composition, inverses); sets (operations, subsets, power sets, cardinality, countability); relations (equivalence relations, partial orders, quotients).
- Phase IV — Advanced Modern Structures (Modules 10–12): Groups and rings; linear algebra (vector spaces, independence, bases); differential calculus (limits, continuity, and the derivative, scoped to the elementary single-variable case).
Course Materials
- Primary Texts: The Mechanics of Proof by Heather Macbeth (hrmacbeth.github.io/math2001) and Mathematics in Lean by the Lean Community (leanprover-community.github.io/mathematics_in_lean).
- Supplementary: Prove It: A Structured Approach (UBC) — personal.math.ubc.ca/~PLP
- Software Stack: Lean 4 Theorem Prover with Visual Studio Code and the official Lean 4 extension.