Vertex Operator Algebras in Lean: a formal library and its companion book
Source: arxiv.org/abs/2611.06616
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2611.06616
curl -X POST /api/v1/records/arxiv/2611.06616/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2611.06616/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'