2 papers
math.CA2026
Formalizing Carleson's Theorem in Lean
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +11
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 m…
cs.PL2025
Growing Mathlib: maintenance of a large scale mathematical library
Anne Baanen, Matthew Robert Ballard, Johan Commelin +3
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for ch…