BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The Carleson Project: Formalization and Collaboration - Floris van
  Doorn (Universität Bonn)
DTSTART:20250610T091500Z
DTEND:20250610T101500Z
UID:TALK230620@talks.cam.ac.uk
DESCRIPTION:In 1966 Lennart Carleson published a proof of an important the
 orem in harmonic analysis\,that states that the Fourier series converges p
 ointwise to the original function under weakconditions. This result has a 
 notoriously difficult proof\,and while the result has been generalized ove
 r the years\, every found proof is full of intricate details.In my talk I 
 will describe an ongoing formalization project that verifies all the detai
 ls of ageneralized Carleson theorem in Lean. I will in particular reflect 
 on the collaborative natureof this formalization.
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR