Distribution theory is a cornerstone of the theory of partial differential equations. We report on the progress of formalizing the theory of tempered distributions in the interactive proof assistant Lean, which is the first formalization in any proof assistant. We give an overview of the mathematical theory and highlight key aspects of the formalization that differ from the classical presentation. As an application, we prove that the Fourier transform extends to a linear isometry on $L^2$ and we define Sobolev spaces via the Fourier transform on tempered distributions.

翻译：分布理论是偏微分方程理论的基石。我们报告了在交互式证明助手Lean中形式化缓增分布理论的进展，这是首个在任何证明助手中完成的形式化工作。我们概述了相关数学理论，并重点强调了与经典表述存在差异的形式化关键方面。作为应用，我们证明了傅里叶变换可延拓为$L^2$上的线性等距映射，并利用缓增分布上的傅里叶变换定义了索伯列夫空间。