- ID
- 2609.31334
- 分类
- —
- 首次捕获
- 2026-09-28
- 状态
- unread
- 作者
- 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, James Sundstrom, Jeremy Tan
- 信号
- SI 43
信号历史
- 2026-09-28Scholar Inbox · 相关分 43
暂无信号数据
摘要
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.