Syllabus
MA4N1 Theorem Proving with Lean
| Lectures | Room | - | Support classes | Room | ||
|---|---|---|---|---|---|---|
| Mondays | 5pm-6pm | MS.05 | - | TBA | TBA | TBA |
| Tuesdays | 11am-noon | MS.03 | - |
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.
| 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.
Switching from Lean 3 to Lean 4 means rewriting all the code, all the supporting information and all the webpages.
This process is completed for Mathlib, however there are still online resources that talk about Lean and mean 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
