An overview of the liquid tensor experiment
Adam Topaz (University of Alberta)
Abstract: 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.
algebraic geometrynumber theory
Audience: researchers in the topic
Series comments: Description: Research/departmental seminar
Seminar usually meets in-person. For online editions, the Zoom link is shared via mailing list.
Organizers: | Katrina Honigs*, Nils Bruin* |
*contact for this listing |