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 weeks 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.
Mikael de la Salle
