The principal assertion of the spectral theorem is that every bounded normal operator $T$ on a Hilbert space induces (in a canonical way) a resolution $E$ of the identity on the Borel subsets of its spectrum $\sigma(T)$ and that $T$ can be reconstructed from $E$ by an integral. A large part of the theory of normal operators depends on this fact.

Current maintainers:

• Oliver Butterley
• Yoh Tanimoto

We aren't so wise to know for sure how big a task it will be to formalize this theorem but we believe we can make some good progress so we are trying. We also want to practice using the blueprint and github project way of collaborating as projects become larger.

See the project home page and Lean blueprint.

We welcome anyone who wants to be part of this.