Formalizing Carlesons theorem using the Lean proof assistant
Formalizing Carleson's Theorem in Lean
Logic in Computer Science
Summary
Carleson's theorem is a complex mathematical statement that can be challenging to verify by hand. The authors used a tool called Lean, which helps check proofs with computer assistance, to fully formalize this theorem. This means they converted the entire proof into a precise language that a computer can verify without mistakes. Their work involved an extensive collaborative effort and thoughtful planning to organize the project effectively.
What this means in practice
- •For formal methods engineers: Allow formal verification teams to include advanced harmonic analysis results like Carleson's theorem in proofs of software and hardware correctness.
- •For mathematical software developers: Enable builders of automated theorem proving tools to integrate complex mathematical theories validated within Lean for improved capabilities.
Authors
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering, Floris van Doorn, Sébastien Gouëzel, Evgenia Karunus, Edward van de Meent, Pietro Monticone, Jasper Mulder-Sohn, Jim Portegies, Joris Roos, Michael Rothgang, James Sundstrom, Jeremy Tan
Abstract
We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, organization of the project, the blueprint, and the main design decisions behind the formalization. It is the result of a large collaborative effort, written and developed in public.