BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:How to teach Fourier analysis to a large library of formalised mat
 hematics - Yaël Dillies (Stockholm Universitet)
DTSTART:20241205T170000Z
DTEND:20241205T180000Z
UID:TALK223858@talks.cam.ac.uk
CONTACT:Anand Rao Tadipatri
DESCRIPTION:If a < b < c are three numbers such that b - a = c - b\, we ca
 ll a\, b\, c an arithmetic progression. How many integers can I take betwe
 en 1 and n without creating an arithmetic progressions?\n\nThis question w
 as asked in the 1930s by Erdös and surprisingly (or unsurprisingly\, if y
 ou know Erdös) was only solved last year. This breakthrough proof involve
 s discrete Fourier analysis\,discrete probability and a lot of ugly calcul
 ations\, the perfect target for a formalisation.\n\nThe theorem prover I a
 m using for this project is Lean. I am basing myself on Mathlib\, the mono
 lithic Lean library of mathematics.\n\nIn the first half of the talk\, I w
 ill explain the story of how I taught Lean Fourier analysis and formalised
  a representative part of the breakthrough proof. I will showcase some key
  contributions to Mathlib that came out of it.\n\nIn the second half of th
 e talk\, I will outline the workflow that I use to contribute vast amounts
  of mathematics to Mathlib quickly and how I juggle four projects simultan
 eously.\n\n=== Hybrid talk ===\n\nJoin Zoom Meeting https://cam-ac-uk.zoom
 .us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1\n\nMeeting ID: 871 
 4336 5195\n\nPasscode: 541180
LOCATION:MR14 Centre for Mathematical Sciences
END:VEVENT
END:VCALENDAR