Virasoro algebra and Sugawara constructions formally in Lean
arXiv:2510.21741
Abstract
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.
16 pages (incl. Appendix)