{
  "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.",
  "abstract_shown": true,
  "affiliations": [],
  "article_type": null,
  "arxiv": "2609.31334",
  "author_total": 14,
  "authors": [
    {
      "name": "Lars Becker"
    },
    {
      "name": "María Inés de Frutos-Fernández"
    },
    {
      "name": "Leo Diedering"
    },
    {
      "name": "Floris van Doorn"
    },
    {
      "name": "Sébastien Gouëzel"
    },
    {
      "name": "Evgenia Karunus"
    },
    {
      "name": "Edward van de Meent"
    },
    {
      "name": "Pietro Monticone"
    },
    {
      "name": "Jasper Mulder-Sohn"
    },
    {
      "name": "Jim Portegies"
    },
    {
      "name": "Joris Roos"
    },
    {
      "name": "Michael Rothgang"
    },
    {
      "name": "James Sundstrom"
    },
    {
      "name": "Jeremy Tan"
    }
  ],
  "bibtex": "https://research.draconitic.com/paper/5pv566y09sw40.bib",
  "cited_by": 0,
  "doi": "10.48550/arxiv.2609.31334",
  "fulltext_url": null,
  "id": "5pv566y09sw40",
  "issns": [],
  "landing_url": "https://hal.science/hal-05768342v1",
  "language": "en",
  "licence": "CC-BY-4.0",
  "licence_label": "CC BY 4.0",
  "licence_source": "article",
  "licence_url": "https://creativecommons.org/licenses/by/4.0/",
  "metadata_licence": "CC0-1.0",
  "native_subjects": [
    [
      "arxiv",
      "cs.LO"
    ],
    [
      "arxiv",
      "math.CA"
    ],
    [
      "hal",
      "0.info"
    ],
    [
      "hal",
      "0.math"
    ],
    [
      "hal",
      "1.info.info-lo"
    ],
    [
      "hal",
      "1.math.math-ca"
    ],
    [
      "openalex",
      "1702|Logic, programming, and type systems"
    ]
  ],
  "openalex": "W7214661958",
  "pdf_url": "https://hal.science/hal-05768342/document",
  "pmcid": null,
  "pmid": null,
  "published": "2026-09-25",
  "publisher": null,
  "ris": "https://research.draconitic.com/paper/5pv566y09sw40.ris",
  "sources": [
    {
      "first_seen": "2026-10-30T12:17:42Z",
      "native_id": "hal-05768342",
      "source": "hal",
      "url": "https://hal.science/hal-05768342v1"
    },
    {
      "first_seen": "2026-10-30T12:24:57Z",
      "native_id": "2609.31334",
      "source": "arxiv",
      "url": "https://arxiv.org/abs/2609.31334"
    }
  ],
  "subjects": [
    {
      "field": "mathematics",
      "origin": "arxiv:math.CA",
      "subfield": "analysis-pdes"
    }
  ],
  "title": "Formalizing Carleson's Theorem in Lean",
  "title_text": "Formalizing Carleson's Theorem in Lean",
  "type": "preprint",
  "updated_at": "2026-10-30T12:24:57Z",
  "url": "https://research.draconitic.com/paper/5pv566y09sw40",
  "venue": "HAL",
  "versions": []
}