# 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