BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Adam Topaz (University of Alberta)
DTSTART:20221110T233000Z
DTEND:20221111T003000Z
DTSTAMP:20260422T053453Z
UID:SFUQNTAG/76
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/SFUQNTAG/76/
 ">An overview of the liquid tensor experiment</a>\nby Adam Topaz (Universi
 ty of Alberta) as part of SFU NT-AG seminar\n\nLecture held in K-9509.\n\n
 Abstract\nIn December 2020\, Peter Scholze proposed a challenge to formall
 y verify a theorem he and Dustin Clausen proved about the real numbers in 
 the context of condensed mathematics\, saying it might be his "most import
 ant theorem to date." I was part of the group who took on this challenge\,
  using the Lean3 interactive theorem prover and its formally verified math
 ematics library `mathlib`. We completed the challenge in July 2022. In thi
 s talk\, I will give a broad overview of condensed/liquid mathematics and 
 the corresponding formalization in Lean. No background in condensed mathem
 atics or interactive theorem provers will be necessary for this talk.\n
LOCATION:https://researchseminars.org/talk/SFUQNTAG/76/
END:VEVENT
END:VCALENDAR