Time: Fridays 15:00-17:00
Place: Y27 H25
Talks:
29.10: Condensed mathematics, by Tim.
5.11: Locally compact abelian groups, by Rizacan.
12.11: Solid mathematics, by Felix.
19.11: Analytic rings, by Ran.
26.11: Liquid modules I - Signed Radon measures, by Emil.
3.12: Liquid modules II - $\mathcal{M}$-complete $\mathbb{R}$-vector spaces, by Emil.
10.12: Liquid modules III - $\mathcal{M}$-complete is not enough, by Felix.
17.12: Liquid modules IV - $\mathbb{R}$ is analytic, by special guest Johan Commelin.
Time: Thursday 16.12.2021, 16:15.
Place: Y27 H12.
Title: The Liquid Tensor Experiment.
Speaker: Johan Commelin, Albert-Ludwigs-Universität Freiburg.
Abstract:
In December 2020, Peter Scholze posed a challenge to formally verify the main theorem on liquid $\mathbb{R}$-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 in a couple of months 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.