Syllabus
Possible weekly topics – outdated
This is a week-by-week breakdown of possible topics for the MA4N1 Theorem Proving with Lean. It is a highly susceptible to changes!
A more stable, periodically updated, syllabus is here.
Week 1 — Introduction to Lean
- Accessing Lean
- installing on a personal computer,
- online GitPod setup,
- online Lean server.
- Resolve potential issues
- installation,
- downloading course material.
- Basic introduction to Lean
- syntax,
- the tactic state,
- what are tactics,
- structuring proofs.
Week 2 — Logic in Lean
and,or,not, implications,iff,- using tactics in proofs.
Week 3 — Sets I
- Encoding of sets,
- relation to Type theory,
- proving basic facts about sets,
- more tactics.
Week 4 — Real numbers
- Simple identities,
- basic manipulations,
- more complicated identities,
- introduction to absolute values.
Week 5 — Inequalities and absolute values
- Dealing with inequalities in Lean,
- initial equivalences,
- mixing inequalities and absolute values.
Week 6 — Formalising limits
- First properties,
- limits of sums, differences, products…
Week 7 — Functions
- Injectivity and surjectivity,
- contrasting Type theory and Set theory.
Week 8 — Sets II
- Subsets, membership, complements,
- unions, intersections,
- images and inverse images.
Week 9 — Finite sets
- Induction,
- using finite sets classically.
Week 10 — Project-related questions
Addressing specific issues arising from working on the projects.
Back to the Theorem Proving with Lean webpage
Back to the Mathlib project for the module
