Vertex Operator Algebras in Lean: a formal library and its companion book
Abstract
We present LeanVOA, a Lean 4 library for the theory of vertex operator algebras (VOAs), together with a companion book that sets each formalized result next to its textbook statement. The library constructs the Moonshine module Vnatural and formalizes Zhu's modular invariance, Huang's tensor categories with the Verlinde formula, the Gannon-Rayhaun classification of c=1 VOAs, and classical freeness of the boundary admissible Lk(sl2) (Arakawa-Dai) and of the minimal models M(2,2m+3) (van Ekeren-Heluani). It also contains new results: graded first-order rigidity of all Virasoro minimal models and of Lk(sl2) at every admissible level; classical freeness of L−3/2(sl3), and of the other members of the Deligne series under stated assumptions; and a proof that graded unitarity of the boundary admissible Lk(sl2) implies that of the minimal models M(2,2n+1). The library declares no axiom of its own.
Related
- Classification of Strongly Rational Vertex Operator Algebras with Central and Effective Central Charge One
- Reverse Module Categories of Vertex Operator Algebras
- Classification and C2-cofiniteness of rational vertex operator algebras generated in low conformal weights
- Vector Bundles of Coinvariants for Admissible Affine Vertex Operator Algebras
- Classification of Rational c=1 Vertex Operator Algebras and Vertex Operator Superalgebras
BibTeX
@misc{popov2026vertex,
title = {{Vertex Operator Algebras in Lean: a formal library and its companion book}},
author = {Fedor K. Popov and Leonardo Rastelli},
howpublished = {arXiv},
year = {2026},
month = nov,
doi = {10.48550/arxiv.2611.06616},
eprint = {2611.06616},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2611.06616},
}
RIS
TY - UNPB
TI - Vertex Operator Algebras in Lean: a formal library and its companion book
AU - Fedor K. Popov
AU - Leonardo Rastelli
PY - 2026
DA - 2026/11/04
PB - arXiv
DO - 10.48550/arxiv.2611.06616
UR - https://arxiv.org/abs/2611.06616
AB - We present LeanVOA, a Lean 4 library for the theory of vertex operator algebras (VOAs), together with a companion book that sets each formalized result next to its textbook statement. The library constructs the Moonshine module V^natural and formalizes Zhu's modular invariance, Huang's tensor categories with the Verlinde formula, the Gannon-Rayhaun classification of c=1 VOAs, and classical freeness of the boundary admissible L_k(sl_2) (Arakawa-Dai) and of the minimal models M(2,2m+3) (van Ekeren-Heluani). It also contains new results: graded first-order rigidity of all Virasoro minimal models and of L_k(sl_2) at every admissible level; classical freeness of L_−3/2(sl_3), and of the other members of the Deligne series under stated assumptions; and a proof that graded unitarity of the boundary admissible L_k(sl_2) implies that of the minimal models M(2,2n+1). The library declares no axiom of its own.
ER -