Virasoro algebra and Sugawara constructions formally in Lean
Kalle Kyt\"ol\"a
TL;DR
This paper formalizes the Virasoro algebra and Sugawara constructions within the Lean proof assistant, providing rigorous, machine-verified proofs of these advanced algebraic structures and their representations.
Contribution
It introduces a formalization of the Virasoro algebra and Sugawara constructions in Lean, advancing the use of proof assistants in infinite-dimensional Lie algebra research.
Findings
Successful formalization of the Virasoro algebra in Lean
Construction of representations via Sugawara methods
Enhanced rigor in infinite-dimensional Lie algebra proofs
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.