Vertex Operator Algebras in Lean: a formal library and its companion book

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^ 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ₖ(sl₂) (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ₖ(sl₂) at every admissible level; classical freeness of L-3/2(sl₃), and of the other members of the Deligne series under stated assumptions; and a proof that graded unitarity of the boundary admissible Lₖ(sl₂) implies that of the minimal models $M(2,2n+1)$. The library declares no axiom of its own.