Colloquium ICJ

Liquid Tensor Experiment

par Johan Commelin

Europe/Paris
En présentiel (UCBL-Braconnier)

En présentiel

UCBL-Braconnier

21 av Claude Bernard, 69100 VILLEURBANNE
Description
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.

Organisé par

Mikael de la Salle