Upcoming lectures

Intercity number theory seminar

11:00–12:00

Anne Baanen VU, Introduction to formalizing number theory

Libraries of formalized mathematics are covering more and more definitions and theorems. This talk introduces the essential concepts of formalizing mathematics, with a special focus on number theory, from the way computer languages can represent proofs, via the current state of formal libraries, to the big questions of the field of formalization. No previous knowledge of formalization or foundations of mathematics is required for this talk.

13:15–14:15

Manuel Eberl Innsbruck, How to avoid bad points in contour integration, rigorously

In this talk I will first give an overview over recent efforts to formalise the foundations of analytic number theory in the proof assistant Isabelle/HOL: Dirichlet series, the Prime Number Theorem, elliptic functions, modular functions and modular forms, etc. In particular, I will highlight some of the difficulties we encountered in the process of formalising this material. For the main part of the talk, I will focus on one particular issue that is always glossed over on paper but that is at first glance very painful in formalisation: the deformation of an integration contour to avoid singularities.

14:30–15:30

Alex Best VU, Formalization in number theory, past, present and future

16:00–17:00

Johan Commelin Freiburg, Liquid Tensor Experiment

In December 2020, Peter Scholze posed a challenge to formally verify the main theorem on liquid ℝ-vector spaces, which is part of his joint work with Dustin Clausen on condensed mathematics. I took up this challenge with a team of mathematicians to verify the theorem in the Lean proof assistant. Half a year later, we reached a major milestone, and our expectation is that shortly we will have completed the full challenge. In this talk I will give a brief motivation for condensed/liquid mathematics, a demonstration of the Lean proof assistant, and discuss our experiences formalizing state-of-the-art research in mathematics.

Intercity seminar

Intercity / Getaltheorie in het Vlakke Land