Skip to ContentSkip to Navigation
Research Bernoulli Institute Calendar

Colloquium Mathematics - Sander Dahmen, VU Amsterdam

When:We 29-05-2024 16:00 - 17: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.