spectral-thm-lean We carry out a complete formalization of the spectral theorem in Lean, for both bounded and unbounded linear operators over some Hilbert space H.