Formalizing Carleson's Theorem in Lean
En palabras de los autores
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.
Resultado principalEl resumen no menciona limitaciones.
Apareció: lunes, 28 de septiembre. arXiv. Preprint, todavía sin revisión por pares.
Comentario de los autores: 32 pages, feedback welcome