Calculational proofs about infinite-dimensional Lie algebras such as the Virasoro algebra and Sugawara constructions have not been formally verified, despite their importance in mathematical physics and conformal field theory.

The authors formalize in Lean the construction of the Virasoro algebra as a central extension of the Witt algebra associated with a nontrivial 2-cocycle. They also formalize representations of the Virasoro algebra via Sugawara constructions. The work involves encoding the relevant infinite-dimensional algebraic structures and verifying the calculational proofs that establish the cocycle condition and representation properties.

The formalization successfully constructs the Virasoro algebra and its Sugawara representations in Lean, providing machine-checked verification of these infinite-dimensional Lie algebra constructions.