Liquid Tensor Experiment

par Johan Commelin

lundi 9 mai 2022, 16:15 → 17:15 Europe/Paris

En présentiel (UCBL-Braconnier)

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.