BEGIN:VCALENDAR
VERSION:2.0
PRODID:icalendar-ruby
CALSCALE:GREGORIAN
METHOD:PUBLISH
BEGIN:VTIMEZONE
TZID:Europe/Vienna
BEGIN:DAYLIGHT
DTSTART:20260329T030000
TZOFFSETFROM:+0100
TZOFFSETTO:+0200
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=3
TZNAME:CEST
END:DAYLIGHT
BEGIN:STANDARD
DTSTART:20261025T020000
TZOFFSETFROM:+0200
TZOFFSETTO:+0100
RRULE:FREQ=YEARLY;BYDAY=-1SU;BYMONTH=10
TZNAME:CET
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
DTSTAMP:20260415T110114Z
UID:1774863000@ist.ac.at
DTSTART:20260330T113000
DTEND:20260330T123000
DESCRIPTION:Speaker: Floris van Doorn\nhosted by Matthew Kwan\nAbstract: Le
 an is a proof assistant which has a large mathematical library containing 
 results from most areas of mathematics. It contains a good foundation to 
 verify current research problems in various areas of mathematics\, and en
 ables new collaborative projects.In this talk I will give an overview of L
 ean and its mathematical library Mathlib\, and describe some of the exciti
 ng formalization projects in this area. In particular\, I will describe a
  recently finished project formalizing a generalization of Carleson's 196
 6 theorem in harmonic analysis\, about the pointwise convergence of Fourie
 r series. This is a major result in harmonic analysis with a difficult pr
 oof\, and this result has been fully verified in Lean. The formalization 
 was a large collaborative project with 17 main contributors.
LOCATION:ISTA | Central Building | Raiffeisen Lecture Hall\, ISTA
ORGANIZER:diana.zubcevic@ista.ac.at
SUMMARY:Floris van Doorn: Lean: Collaboration Using Formalization
URL:https://talks-calendar.ista.ac.at/events/5761
END:VEVENT
END:VCALENDAR