Intercity Number Theory Seminar

2022

Intercity number theory seminar

13 May, Utrecht. Morning: Buys Ballotgebouw room 209; afternoon: Koningsbergergebouw room 1.50 PANGEA
11:00–12:00
Florian Wilsch IST Austria, Integral points of bounded height on a certain toric variety
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.
13:15–14:15
Miriam Kaesberg Goettingen, On Artin’s Conjecture: Pairs of Additive Forms
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.
14:30–15:30
Nirvana Coppola VU, Coleman integrals over number fields: a computational approach
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.
15:45–16:45
Vladimir Mitankin Hannover, Semi-integral points on quadrics
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 number theory seminar

3 June, VU Amsterdam. Main building (Hoofdgebouw), room HG–06A32
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

1 September, Groningen. Linked to the conference Curves over finite fields and arithmetic of K3 surfaces for Jaap Top's 62nd birthday – please register if you plan to attend!

Intercity / Getaltheorie in het Vlakke Land

23 September, Utrecht.