Condensed Mathematics and Analytic Geometry

Fall 2021 — University of Zürich

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.

Bonus Talk

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.