An introduction to proof assistants: a mini course about mathematical formalization

External homepage

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 timeSpeakerTitle
WedNov 0214:30Riccardo BrascaExamples and exercises about formalization mathematics in Lean
ThuOct 2718:00Riccardo BrascaThe Lean proof assistant
WedOct 2618:00Riccardo BrascaAn introduction to formalized mathematics: why it is interesting?
Embed this schedule
Export series to