New Technologies in Mathematics Seminar

Speaker: María Inés de Frutos Fernández, Mathematical Institute, University of Bonn

Title: The Carleson project: A collaborative formalization

Abstract: A well-known result in Fourier analysis establishes that the partial Fourier sums of a smooth periodic function $f$ converge uniformly to $f$, but the situation is a lot more subtle for e.g. continuous functions. However, in 1966 Carleson proved that they do converge at almost all points for $L^2$ periodic functions on the real line. Carleson’s proof is famously hard to read, and there are no known easy proofs of this theorem. As a large collaborative project, we have formalized in Lean a generalization of Carleson’s theorem in the setting of doubling metric measure spaces (proven in 2023), and Carleson’s original result as a corollary. In this talk I will give an overview of the project, with a focus on how the collaboration was organized.