The goal of this workshop is to learn about computer-assisted formalization of mathematics. During the workshop, we will be using Lean, an interactive theorem prover, which is being used by a large community of mathematicians, who are actively building an extensive mathematical library.
No prior experience with Lean or other theorem provers is required. This workshop will have weekly meetings, and is divided into two parts, both of which are optional. The first part will consist of approximately 4 sessions, where we cover the basics of type theory, the mathematical foundation on which Lean is built, as well as Lean's syntax. The main activity will be programming sessions, where we go through various exercises, proving theorems about numbers, algebraic structures, and other undergraduate topics.
For the second part of the workshop, together we will pick an approachable theorem for us to formalize, as well as its dependencies, that we can contribute to Lean's mathematical library.
This workshop is organized by PhD students Daan van Gent and Jesse Vogel.
The contents of the schedule are not fixed, and can be changed depending on the needs of the participants.
| Week | Activity |
|---|---|
| 38 | Presentation on type theory in Lean (Jesse) (Notes | Slides | Demo file) Introduction to the Natural Number Game |
| 39 |
Installing Lean
Choose some exercises you like:
|
| 40 |
Choose some exercises you like:
|
| 41 |
Choose some exercises you like:
|
| ≥ 42 | Representation Theory in Lean (GitHub repository, Lecture notes) |