If a
This question was asked in the 1930s by Erdös and surprisingly (or unsurprisingly, if you know Erdös) was only solved last year. This breakthrough proof involves discrete Fourier analysis,discrete probability and a lot of ugly calculations, the perfect target for a formalisation.
The theorem prover I am using for this project is Lean. I am basing myself on Mathlib, the monolithic Lean library of mathematics.
In the first half of the talk, I will 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.
In the second half of the talk, I will outline the workflow that I use to contribute vast amounts of mathematics to Mathlib quickly and how I juggle four projects simultaneously.
=== Hybrid talk ===
Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180
