Syllabus
MA4N1 Theorem Proving with Lean
| Lectures | Room | - | Support classes | Room | ||
|---|---|---|---|---|---|---|
| Mondays | 5pm-6pm | MS.05 | - | Thursdays | 4pm-5pm | B1.01 |
| Tuesdays | 11am-noon | MS.03 | - |
| Office hours | Room | |
|---|---|---|
| Mondays (odd weeks) | 4pm-5pm | C2.13 |
| Tuesdays (even weeks) | noon-1pm | C2.13 |
Assessment
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.
Note: 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.
Available pages
- Current syllabus
- MA4N1 Theorem Proving with Lean
- Introduction to
Theorem Proving with Lean - Initial tactic, brackets and basic logic symbols
- Commonly used symbols
- Basic Lean4 syntax
- What tools do I have to tease information out of Lean4?
- Sample Lean file
- Projects and stubs of ideas
- Creating a new project depending on
Mathlib - Possible weekly topics – outdated
- FAQ
Back to the Mathlib project for the module
