← All papers
The continuous functional calculus in Lean
math.OA
Jan 26, 2025 · v1
TL;DR
Formalizes the continuous functional calculus for C*-algebras in Lean, merged into Mathlib.
Abstract
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.
Problem
The continuous functional calculus is the most fundamental construction in the theory of C*-algebras and operator algebras, but it had not been formalized in any proof assistant.
Approach
The authors formalize the continuous functional calculus in Lean 4, constituting the first such formalization in any proof assistant. The implementation is merged into Mathlib. The paper describes design decisions in the formalization that proved important for usability.
Results
The formalization is the first of the continuous functional calculus in any proof assistant and is already available in Mathlib for downstream use.