Online talk on managing a project depending on Mathlib

Stream: general

[Yaël Dillies]

For anyone interested, I will be giving a talk on the formalisation of contemporary additive combinatorics AND on my workflow for contributing to Mathlib. The talk will be given in person in Cambridge at 2024-12-05T17:00:00Z and will also be retransmitted on Zoom (and recorded, but I suggest you don't rely on that option since it might be a month before the recording is available)

[Yaël Dillies]

The details are here. Copied out for your convenience:

[Yaël Dillies]

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.

[Yaël Dillies]

Join Zoom Meeting https://cam-ac-uk.zoom.us/j/87143365195?pwd=SELTNkOcfVrIE1IppYCsbooOVqenzI.1
Meeting ID: 871 4336 5195
Passcode: 541180