Virasoro algebra and Sugawara constructions formally in Lean
Quantum Algebra
2025-10-28 v1 Mathematical Physics
math.MP
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.
Cite
@article{arxiv.2510.21741,
title = {Virasoro algebra and Sugawara constructions formally in Lean},
author = {Kalle Kytölä},
journal= {arXiv preprint arXiv:2510.21741},
year = {2025}
}
Comments
16 pages (incl. Appendix)