{"id":"arxiv/2611.06616","url":"https://arxiv.org/abs/2611.06616","tags":["math.QA","hep-th"],"score":0,"title":"Vertex Operator Algebras in Lean: a formal library and its companion book","domain":"math.QA","source":"arxiv","authors":["Fedor K. Popov","Leonardo Rastelli"],"reviews":0,"subject":"math.QA","summary":"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(\\mathfrak{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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-11-04","reactions":{}}