Colloquium Mathematics - Sander Dahmen, VU Amsterdam
| When: | We 29-05-2024 16:00 - 18:00 |
| Where: | 5161.0105 Bernoulliborg |
Title: Formalizing Mathematics
Abstract:
Proof assistants, such as Coq, Isabelle, and Lean, are software tools that assist in rigorously expressing mathematical statements and their proofs in a formal logical language. Mathematics that has been formalized in this way spans many different fields. In this talk, after an extensive general introduction, we will discuss some past, present, and future formalization work in number theory. During the second half, we will focus mostly (but not exclusively) on the Lean proof assistant.