BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//CERN//INDICO//EN
BEGIN:VEVENT
SUMMARY:Collaboration using formalization in mathematics [Lecture]
DTSTART:20260507T070000Z
DTEND:20260507T080000Z
DTSTAMP:20260518T072100Z
UID:indico-event-1297@math-events.uni-bonn.de
DESCRIPTION:Speakers: Floris van Doorn (MI Bonn)\n\nFormalization of mathe
 matics is a rapidly growing field that has seen exciting results in recent
  years\, such as the formalization of the main theorem in condensed mathem
 atics\, Gromov's h-principle and Carleson's theorem. These results are for
 malized in Lean\, building on its mathematical library Mathlib. These proj
 ects are often a collaboration between many people\, more than is usual fo
 r a typical mathematical paper.\nIn this talk I will give an overview of L
 ean and its mathematical library Mathlib\, and focus on the Carleson proje
 ct that I led last year. In this project we formalized a generalization of
  Carleson's 1966 theorem in harmonic analysis about the pointwise converge
 nce of Fourier series. This result has a notoriously difficult proof\, whi
 ch is fully verified in Lean. The formalization was a large collaborative 
 project with 17 main contributors.\n\nhttps://math-events.uni-bonn.de/even
 t/1297/
LOCATION:Endenicher Allee 60 / Lipschitzsaal (Mathezentrum)
URL:https://math-events.uni-bonn.de/event/1297/
END:VEVENT
END:VCALENDAR