November 7, 2023
Title: Aspects of the Liquid Tensor Experiment (MI talk)
Speaker: Johan Commelin
The Liquid Tensor Experiment is a project that formally verified the main theorem of liquid vector spaces by Clausen and Scholze, following up on a challenge by Scholze on Buzzard's XenaProject blog. In this talk I will explain the thrust of this main theorem and share some mathematical insights gained from my protracted battle with its proof.