Tomorrow we're hosting our first official NYC Lean talk, kicking things off with Gregory Wickham on his formalization of the Gelfand–Naimark–Segal (GNS) construction. From his abstract:
I formalized the Gelfand–Naimark–Segal (GNS) construction using the proof assistant Lean. The GNS construction is a method for constructing a Hilbert space and a ∗-homomorphism from a C∗-algebra into the algebra of bounded operators on that Hilbert space. The GNS construction is an essential step in the proof [of] the Gelfand–Naimark theorem, which is a foundational theorem in the theory of C∗-algebras. This formalization has been “peer-reviewed” in the sense in which Lean formalization projects are reviewed, meaning that it has been merged into Mathlib, the canonical, open-source library of mathematics in Lean.
Wickham's work formalizes a foundational result about the representation of linear functionals on infinite-dimensional complex vector spaces. Its central objects, C∗-algebras, impose additional structure on the traditional Banach spaces from functional analysis. These results play an important role in mathematical physics:
Algebraic Quantum Field Theory (AQFT) — the most successful attempt to reformulate QFT axiomatically — employs only bounded operators. It builds upon work in the 1940s by Gelfand, Neumark, and in particular Segal, who tried to describe quantum physics in terms of C∗-algebras.
Wickham completed the formalization as his senior thesis at Harvey Mudd College, advised by Lucas Bang. His thesis and the poster are available below. It was a collaborative effort, with extensive feedback and contributions from fellow Lean community members Jireh Loreaux and Monica Omar. For more details, come to his talk tomorrow at Tower 49, or watch the video on our YouTube channel.