How to teach Fourier analysis to a large library of formalised mathematics

Add to your list(s) Download to your calendar using vCal

• Yaël Dillies (Stockholm Universitet)
• Thursday 05 December 2024, 17:00-18:00
• MR14 Centre for Mathematical Sciences.

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.

=== Hybrid talk ===

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1

Meeting ID: 871 4336 5195

Passcode: 541180

This talk is part of the Formalisation of mathematics with interactive theorem provers series.

This talk is included in these lists:

• All CMS events
• All Talks (aka the CURE list)
• CMS Events
• Cambridge talks
• DPMMS Lists
• DPMMS Pure Maths study groups
• DPMMS info aggregator
• DPMMS lists
• Department of Computer Science and Technology talks and seminars
• Formalisation of mathematics with interactive theorem provers
• Hanchen DaDaDash
• Interested Talks
• MR14 Centre for Mathematical Sciences
• School of Physical Sciences
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.