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 in the summer of 2022 we have completed the full challenge.
In this talk I will give a brief motivation for condensed/liquid mathematics, report on our experiences formalizing state-of-the-art research in mathematics, and discuss attempts to conceptualize the proof of Clausen--Scholze.
Copyright. All Rights Reserved.