Liquid Tensor Experiment

Vortrag von Dr. Johan Commelin

Sprecher eingeladen von: Prof. Dr. Joseph Ayoub

Datum: 16.12.21  Zeit: 16.15 - 17.45  Raum: 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