Lectures | Room | - | Support classes | Room | ||
---|---|---|---|---|---|---|
Mondays | 5pm-6pm | MS.05 | - | Tuesdays | 4pm-5pm | D1.07 |
Tuesdays | 11am-noon | MS.03 | - |
The assessment for the module is 100% coursework, based on group projects.
Two submissions are during Term 1.
The final submission is at the end of January, in Term 2.
All deadlines are on Thursdays at noon of the specified weeks.
Assessment | Submission type | Deadline | Weighting |
---|---|---|---|
Outline of formalization | Group | Week 5 | 10% |
Video of personal contribution (up to 4 minutes) | Individual | Week 9 | 20% |
Final formalization | Group | Term 2, Week 3 | 70% |
You can find some ideas for what might constitute a “toy project” here.
The Lean 4 project containing the Lean files for the lectures is here.
The module is based on the proof assistant Lean 4. We will use Mathlib, the mathematical library of Lean 4.
You can find ways to interact with Lean and Mathlib on the Mathlib webpage.
Lean 3
vs Lean 4
Lean 4 is the latest version of Lean.
Most online resources use Lean 4. Very few may still talk about Lean 3. In this module, we will only work with Lean 4.
Theorem Proving with Lean
Mathlib