## SFU Number Theory and Algebraic Geometry Seminar: Adam Topaz

• Date: 11/10/2022
• Time: 15:30
Lecturer(s):
Location:

Simon Fraser University

Topic:

An overview of the liquid tensor experiment

Description:

In December 2020, Peter Scholze proposed a challenge to formally verify a theorem he and Dustin Clausen proved about the real numbers in the context of condensed mathematics, saying it might be his "most important theorem to date." I was part of the group who took on this challenge, using the Lean3 interactive theorem prover and its formally verified mathematics library mathlib. We completed the challenge in July 2022. In this talk, I will give a broad overview of condensed/liquid mathematics and the corresponding formalization in Lean. No background in condensed mathematics or interactive theorem provers will be necessary for this talk.

Other Information:

Location: SFU (K-9509)