def fact : Nat → Nat
| 0 => 1
| k + 1 => (k + 1) * fact k
#check fact -- fact : Nat → Nat
#check fact 5 -- fact 5 : Nat
#eval fact 5 -- 120- Target audience: Bachelor students.
- Language of instruction: English.
- Supervised by: Judith Ludwig & Florent Schaffhauser.
- Time and place: Thursday 2:00-4:00 PM, in SR 3 (INF 205).
- Zulip channel.
Topic and goal
In this seminar, we focus on the formalisation of mathematics in an interactive theorem prover, using the Lean programming language. Our goal will be to learn what it means to write a formal proof and have the computer validate it, or even assist us with it.
Organisation
- In the first part of the seminar, each session will combine an introduction to a particular topic regarding the use of proof assistants, followed by hands-on computer practice. Participants will be encouraged to work in pairs.
- In the second part of the seminar, participants will work in pairs and focus on specific projects. Each team will deliver a final presentation on their project at the end of the semester.
- Attendance is mandatory.
| Date | Topic |
|---|---|
| 17.04 | Introduction to formalisation and the Lean syntax. |
| 24.04 | Propositions as types and Basic tactics. |
| 08.05 | Lean install + Git tutorial. |
| 15.05 | Advanced Lean tactics + Mathlib. |
| 22.05 | More Mathlib + Choice of topics for the projects. |
| 05.06 | Tutorial / Project work. |
| 12.06 | Tutorial / Project work. |
| 26.06 | Project work (in class). |
| 03.07 | Project work (in class). |
| 10.07 | Final presentations. |
| 17.07 | Final presentations. |