In December 2020, Peter Scholze posed a challenge to formally verify the main theorem on liquid real 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 have reached a major milestone, and our expectation is that we are roughly halfway done with the challenge.
Talk 1 (July 2). The first in this series of three talks will be a colloquium-style talk aimed at a general audience. 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.
Talk 2 (July 9). In the second talk I will give more background on how Lean works. We will see how different components play together to create an extendable interactive proof assistant.
Talk 3 (July 16). The third talk will give an overview of the proof that we are formalizing. The proof consists of an intricate mix of functional analysis and homological algebra. Instead of getting dragged down in technical inequality estimates, I will try to give a high-level picture of the techniques involved. In particular, I will discuss a simplification of Breen–Deligne resolutions that was discovered during this project.
Addendum. I have attempted to write a sketch of the proof of the liquid structure on the real numbers. The original proof is 32 pages long. I hope that the 10 pages can serve as some roadmap to understanding this proof.
[sketch.pdf] [talk3.mp4]