Workshop
talk cancelled
- Floris van Doorn
Abstract
In recent years, formalization has received more attention from mathematicians because of success stories such as the Liquid Tensor Experiment, which formalized a deep result from condensed mathematics in Lean. I will discuss the Carleson project, an ongoing formalization that verifies a modern generalization of Lennart Carleson's 1966 theorem in harmonic analysis about the pointwise convergence of Fourier series under weak conditions. Carleson's original proof is notoriously difficult, and all subsequent proofs required a lot of intricate details. In particular, I will reflect on the collaborative nature of this formalization.
