Skip to content
DraconiticResearch
Search Sources API
201,683 studies31 sourcesUpdated 3 min ago
PreprintCC BY 4.0HAL

Formalizing Carleson's Theorem in Lean

  • 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
2 more authors
  • James Sundstrom
  • Jeremy Tan
Open at sourcePDFDOICite

Abstract

We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, the 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.

Related

  1. Formalizing Fefferman's Official Periodic Navier-Stokes Problem (B) in Lean 4: Global Linear Strain Exclusion on T3, Biot-Savart Direction Depletion Identities, and Conditional Reductions via Beale-Kato-Majda
    Benjamin Frohman
    Zenodo (CERN European Organization for Nuclear Research)PreprintLicence not stated5 citedGeneral mathematicsOpenAlex
  2. Formalizing Flag Algebras in Lean
    Gyeongwon Jeong, Seonghun Park, Jihoon Hyun +2
    arXivPreprintCC BY 4.0Full text1 citedCombinatorics & discrete mathematicsarXiv
  3. A stochastic Carleson embedding theorem with constant e and the vector of Riesz transforms
    Komla Domelevo, Johanna Fladung, Spyridon Kakaroumpas +2
    arXivPreprintCC BY 4.0Full textAnalysis & PDEsProbabilityarXiv
  4. A Formal Proof of Riemann Hypothesis from Existence Alone, the Sign Excepted by Theorem: The Constructed Witness, the Identity Cone over the Fixed Locus, the Grounded Counter-Model, and the Cure Theorem Proved in Lean 4 and Re-executed in Fortran
    Mohammad Islam
    PhilPapers (PhilPapers Foundation)Peer-reviewedLicence not statedFull text10 citedAlgebra & number theoryOpenAlex
  5. Formalization of Sullivan's No Wandering Domains Theorem in Lean
    Ziang Li, Yusheng Luo
    arXivPreprintarXiv licenceFull textMathematical physicsarXiv

Cite

BibTeXRIS
BibTeX
@misc{becker2026formalizing,
  title = {{Formalizing Carleson's Theorem in Lean}},
  author = {Lars Becker and María Inés de Frutos-Fernández and Leo Diedering and Floris van Doorn and Sébastien Gouëzel and Evgenia Karunus and Edward van de Meent and Pietro Monticone and Jasper Mulder-Sohn and Jim Portegies and Joris Roos and Michael Rothgang and James Sundstrom and Jeremy Tan},
  howpublished = {HAL},
  year = {2026},
  month = sep,
  doi = {10.48550/arxiv.2609.31334},
  eprint = {2609.31334},
  archivePrefix = {arXiv},
  url = {https://hal.science/hal-05768342v1},
  note = {CC BY 4.0},
}
RIS
TY  - UNPB
TI  - Formalizing Carleson's Theorem in Lean
AU  - Lars Becker
AU  - María Inés de Frutos-Fernández
AU  - Leo Diedering
AU  - Floris van Doorn
AU  - Sébastien Gouëzel
AU  - Evgenia Karunus
AU  - Edward van de Meent
AU  - Pietro Monticone
AU  - Jasper Mulder-Sohn
AU  - Jim Portegies
AU  - Joris Roos
AU  - Michael Rothgang
AU  - James Sundstrom
AU  - Jeremy Tan
PY  - 2026
DA  - 2026/09/25
PB  - HAL
DO  - 10.48550/arxiv.2609.31334
UR  - https://hal.science/hal-05768342v1
AB  - We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, the 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.
ER  -