# 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**.

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.