COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |
University of Cambridge > Talks.cam > Formalisation of mathematics with interactive theorem provers > How to teach Fourier analysis to a large library of formalised mathematics
How to teach Fourier analysis to a large library of formalised mathematicsAdd to your list(s) Download to your calendar using vCal
If you have a question about this talk, please contact Anand Rao Tadipatri. If a < b < c are three numbers such that b – a = c – b, we call a, b, c an arithmetic progression. How many integers can I take between 1 and n without creating an arithmetic progressions? 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. This talk is part of the Formalisation of mathematics with interactive theorem provers series. This talk is included in these lists:
Note that ex-directory lists are not shown. |
Other listsForum for Youth Participation and Democracy UCL based talks series The Sackler LecturesOther talksOn the Practical cost of Grover for AES Key Recovery Artery: racial ecologies in fluvial Columbia Technology for Bioelectronic Medicine Bohnenblust--Hille inequalities and low-degree learning Gravitational collapse simulations on null cones Vector Quantization in Deep Neural Networks for Speech and Image Processing |