Talk
Liquid Tensor Experiment
Talk by Dr. Johan Commelin
Speaker invited by: Prof. Dr. Joseph Ayoub
Date: 16.12.21 Time: 16.15 - 17.45 Room: Y27H12
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 months 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.
LINK TO ATTEND REMOTELY:
https://seminarlive.math.uzh.ch/semlive/index.php?id=vuestreaming&meetingId=622