在 Lean 中形式化 Carleson 定理
Formalizing Carleson's Theorem in Lean
- Princeton University（普林斯顿大学）
- University of Bonn（波恩大学）
- University of Rennes（雷恩大学）
- Utrecht University（乌得勒支大学）
- Harmonic（哈莫尼克）
- The Hague（海牙）
- Eindhoven University of Technology（埃因霍温理工大学）
- University of Massachusetts Lowell（马萨诸塞大学洛厄尔分校）
- Baruch College（巴鲁克学院）
- National University of Singapore（新加坡国立大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文介绍了在 Lean 证明助手中形式化 Carleson 定理的项目，涵盖数学内容、组织、蓝图及设计决策，是公开协作的成果。
AI中文摘要：
我们展示了在证明助手 Lean 中对 Carleson 定理的形式化。本文描述了该形式化的数学内容、项目组织、蓝图以及主要设计决策。这是大规模协作努力的结果，公开编写和开发。
英文摘要：
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.
