Virasoro algebra and Sugawara constructions formally in Lean

We formalize in Lean certain calculational proofs about infinite-dimensional Lie algebras. Specifically, we construct the Virasoro algebra as a central extension of the Witt algebra associated with a nontrivial 2-cocycle, and we construct representations of the Virasoro algebra by Sugawara constructions.