An introduction to proof assistants: a mini course about mathematical formalization
Mathematics
Universidad de Santiago de Chile (USACH)
| Audience: | General audience |
| Seminar series times: | No fixed schedule |
| Organizers: | Daniel Barrera*, Héctor del Castillo* |
| *contact for this listing |
The goal of this mini-course is to give an introduction to formalization of mathematics. I will explain what formalizing mathematics means and why it is interesting and useful for people interested in "standard" mathematics. I will show how this is done in practice using Lean, one of the several proof assistants available today. This is not a course in logic nor foundations of mathematics, in particular no prior knowledge of these topics is needed.
Upcoming talks
Past talks
| Your time | Speaker | Title | |||
|---|---|---|---|---|---|
| Wed | Nov 02 | 14:30 | Riccardo Brasca | Examples and exercises about formalization mathematics in Lean | |
| Thu | Oct 27 | 18:00 | Riccardo Brasca | The Lean proof assistant | |
| Wed | Oct 26 | 18:00 | Riccardo Brasca | An introduction to formalized mathematics: why it is interesting? | |
Export series to