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

Fedor K. Popov, Leonardo Rastelli

math.QA Nov 4, 2026 · v1 hep-th

Read PDF arXiv abstract Code

TL;DR

Presents LeanVOA, a Lean 4/Mathlib library of about 3.7M lines formalizing vertex operator algebra theory, written by AI agents under human direction.

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 $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 Virasoro minimal models and of $L_k(\mathfrak{sl}_2)$ at every admissible level; classical freeness of $L_{-3/2}(\mathfrak{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(\mathfrak{sl}_2)$ implies that of the minimal models $M(2,2n+1)$. The library declares no axiom of its own.

Problem

Vertex operator algebra theory, including the Moonshine module, Zhu's modular invariance, Huang's tensor categories and recent classification results, had no machine-checked formal development.

Approach

The authors built LeanVOA in Lean 4 on Mathlib. It derives the Borcherds identity from locality, constructs Heisenberg, Virasoro, affine and lattice VOAs, and develops module theory, Zhu's algebra and modular invariance. AI coding agents (Claude, Codex) wrote all of the Lean code under human direction, with AI referee loops reviewing the work. Large finite certificate data is generated by Python and re-checked by kernel reduction. A companion book places each Lean declaration verbatim next to its textbook statement.

Results

The library constructs the Moonshine module, formalizes the Gannon–Rayhaun c=1 classification, and proves the Arakawa–Dai and van Ekeren–Heluani classical-freeness results. It also contains new rigidity, freeness and graded-unitarity results. It spans 11,660 files and about 3.75M lines, uses only Lean's standard axioms, and contains no sorry or native_decide.

Directory	Files	Lines
Classification (c=1)	1,756	1,627,513
DeligneAudit	6,173	1,241,760
Huang	931	183,719
Moonshine	170	55,246

Selected library directories by size

Papers With

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