Summary
In recent years computerized tools for verifying and manipulating proofs have become much more mature, and as a result formalized proofs are playing a meaningful role in mathematical innovation and teaching.
This short program consists of three colloquium talks on major aspects of formalization, in terms of both underlying ideas and concrete implementations, together with a series of workshop-style sessions intended to give participants first-hand knowledge using the Lean language, its mathematical library and associated tools. We aim to provide an introduction to the area for working mathematicians and advanced students in a variety of fields.
Copious quantities of coffee ☕ and space to code and collaborate will be available.
Workshop and talks will be held in the Department of Mathematics, University of Rome Tor Vergata (Via della Ricerca Scientifica 1, 00133 Roma).
Schedule & speakers
| Wed 24/01/2024 | Thu 25/01/2024 | Fri 26/01/2024 | |
|---|---|---|---|
| 10:00-11:00 | workshop | workshop | |
| 11:00-12:00 | ☕ 💻 | ☕ 💻 | |
| 12:00-13:00 | workshop | Colloquium 2 | workshop |
| 13:00-14:30 | 🍽️ | 🍽️ | 🍽️ |
| 14:30-15:30 | workshop | Colloquium 3 | Colloquium 4 |
| 15:30-16:30 | Colloquium 1 | ☕ 💻 | ☕ 💻 |
| 16:30-17:30 | ☕ 🍷 | workshop | workshop |
Session topics (tap to view)
| session | speaker | topics | |
|---|---|---|---|
| 1 | introduction | Riccardo | tutorial on Lean, installation of Lean (if needed), topics in mathlib (ch 1) |
| 2 | basics | Gihan | apply, rewrite, linarith (ch 2) |
| 3&4 | logic | Riccardo | logical connectives and quantifiers (ch 3) |
| 5 | sets, functions | Filippo | intersections, (pre)images, extensionality (ch 4) |
| 6&7 | topology | Floris | topological spaces, filters (ch 9) |
Chapter numbers listed are from Mathematics in Lean.
Speakers
- Riccardo Brasca
- Kevin Buzzard
- Floris van Doorn
- Gihan Marasingha
- Filippo A. E. Nuccio Mortarino Majno di Capriglio
See also the event team page.
Colloquium talks
| speaker | title | |
|---|---|---|
| Colloquium 1 | Filippo A. E. Nuccio Mortarino Majno di Capriglio | TBA |
| Colloquium 2 | Floris van Doorn | TBA |
| Colloquium 3 | Gihan Marasingha | TBA |
| Colloquium 4 | Kevin Buzzard | TBA |
Register
In case you are interested, please register, sooner rather that later, it helps us a lot with the organization! (And it's fine if you change your mind.)
Contact
Contact Oliver Butterley or another of the local organizers for anything practical.
Links
- Getting started with Lean: If you haven't already, get started by installing Lean or using it online.
- Other events of interests: For those who want to go deeper into Lean and mathlib, check out some other Lean events.