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 mathematics

Add 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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2024 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity