Lessons from the Carleson project

Abstract: From June 2024 to July 2025 the Carleson project ran, a community-driven collaboration to formalize a modern generalization of Carleson's theorem, proven by the Bonn harmonic analysis group in 2023. In this talk I will reflect on the project, discuss what lessons we can learn from it, and describe further formalization goals in harmonic analysis.

logic in computer sciencemathematical softwareMathematics

Audience: researchers in the discipline

( slides | video )

Lean Together 2026