标题： 连续函数演算在Lean中 显示英文标题

标题： The continuous functional calculus in Lean

摘要： 连续函数演算可能是算子代数理论中最基本的构造，尤其是在$C^{*}$-代数中。 在这里，我们记录了在Lean中对连续函数演算的形式化，这是任何证明助手中的首次此类形式化。 我们的实现已经合并到Lean的数学库Mathlib中。 我们为不熟悉该主题的人提供了一个数学理论的简要介绍，然后强调了我们在形式化过程中做出的设计决策，这些决策被证明对可用性非常重要。 我们的阐述面向一般的数学读者，并通过揭示发现过程，提供了进入形式化世界的一瞥。 显示英文摘要

摘要： The continuous functional calculus is perhaps the most fundamental construction in the theory of operator algebras, especially $C^{*}$-algebras. Here we document our formalization of the continuous functional calculus in Lean, which constitutes the first such formalization in any proof assistant. Our implementation is already merged into Lean's mathematical library, Mathlib. We provide a brief introduction to the mathematical theory for those unfamiliar with the subject, and then highlight the design decisions in our formalization which proved to be important for usability. Our exposition is aimed at a general mathematical audience and provides a glimpse into the world of formalization by laying bare the discovery process.