## 2021

### Intercity seminar

22 October, Leiden. Sylvius laboratory room 1.4.31, starting at 11:15- 11:15–12:00
- Remy van Dobben de Bruyn Leiden, Equivalent conjectures on independence of ℓ
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:15–15:00
- Margherita Pagano Leiden, An example of a Brauer–Manin obstruction to weak approximation at a prime with good reduction
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:15–16:00
- Daan van Gent Leiden, Indecomposable algebraic integers
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.
- 16:30–17:15
- Pim Spelier Leiden, Geometric quadratic Chabauty on
*X*_{0}(67)^{+}

### Intercity seminar

12 November, Leiden. Snellius building room 401, starting with coffee/tea at 11:00. Live stream via Zoom- 11:15–12:00
- Peter Stevenhagen Leiden, Elliptic curves and primes of cyclic reduction
- 14:15–15:00
- Charlotte Dombrowsky Leiden, An upper bound for packings on spheres
- 15:30–16:15
- Yukako Kezuka MPIM Bonn, On central L-values of twists of the Fermat elliptic curve
- 16:15–17:00
- Eugenia Rosu TU Darmstadt / Leiden, Twists of elliptic curves with complex multiplication

~~Intercity seminar / Getaltheorie in het Vlakke Land / Arithmétique en Plat Pays~~

10 December, Utrecht. **Cancelled**

- 13:15–14:00
- Laurent Berger ENS Lyon, Unlikely intersections for formal groups
- 14:15–15:00
- Michel Rigo Liège, Numeration systems: a link between formal languages and number theory
- 15:30–16:15
- Amita Malik MPIM, Integer partitions analysis
- 16:30–17:15
- Lola Thompson Utrecht, Salem numbers and short geodesics