BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Hannah Scholz (University of Bonn)
DTSTART:20260122T163000Z
DTEND:20260122T170000Z
DTSTAMP:20260420T025624Z
UID:LT2026/34
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/34/">
 Formalisation of CW complexes</a>\nby Hannah Scholz (University of Bonn) a
 s part of Lean Together 2026\n\n\nAbstract\nCW complexes are a class of to
 pological spaces that are of particular importance in algebraic topology. 
 Intuitively\, they are the result of glueing continuous images of discs to
 gether along their boundaries. My talk will concern the classical way of d
 efining them\, close to Whitehead’s original definition. I will first di
 scuss the definition and a particular challenge with typeclass inference t
 hat we faced when implementing it in Lean. Afterwards\, I will report on t
 he current status of CW complexes in Lean and lastly\, I will give a glimp
 se of the mathematically most interesting part of the project: the product
  of CW complexes. All the work that I will be presenting was done together
  with and supervised by Prof. Floris van Doorn.\n
LOCATION:https://researchseminars.org/talk/LT2026/34/
END:VEVENT
END:VCALENDAR