Seminar des SFB/TRR 326 GAUS

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 this summer we 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.

Freitag, den 21. Oktober 2022 um 13:30 Uhr, in INF 205, SR A Freitag, den 21. Oktober 2022 at 13:30, in INF 205, SR A

Der Vortrag folgt der Einladung von The lecture takes place at invitation by Dr. Judith Ludwig