In late 2021, Bloom resolved an old conjecture of Erdős and Graham, showing that in any subset of the positive integers of positive density, there exists a solution to 1/n1 + 1/n2 + … + 1/nk = 1 with all ni distinct. We discuss the formal verification of this proof in the Lean theorem prover, including prerequisites from analytic number theory and Fourier analysis, and an instance of the circle method. This is joint work with Thomas Bloom.
This video is part of the Webinar in Additive Combinatorics series, and this is their YouTube channel.
