Time:

17:00-18:00 July 27, 2021

17:00-18:30 July 29, 2021

Abstract:

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.

The first in this pair 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.

In the second I 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.

Zoom information

Meeting ID: 892 1994 7783

Passcode: 973756

See also

A Nature article on the Liquid Tensor Experiment

https://www.nature.com/articles/d41586-021-01627-2