Ruprecht-Karls-Universität Heidelberg
MoDiMiDoFrSaSo
26 27 28 29 1 2
3
4 5 6 7 8 9 10
11 12 13 14 15 16 17
18 19 20 21 22 23 24
25 26 27 28 29 30 31
Informationen für
„Liquid Tensor Experiment“
Dr. Johan Commelin, Universität Freiburg

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