{"id":"arxiv/2609.27952","url":"https://arxiv.org/abs/2609.27952","tags":["math.QA"],"score":0,"title":"A Lean 4 Verification Report for Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras","domain":"math.QA","source":"arxiv","authors":["Sihai Jin"],"reviews":0,"subject":"math.QA","summary":"We report a Lean 4 formal audit accompanying the paper \"Completing the Arakawa--Moreau Conjecture on Maximal Ideals of Affine Vertex Algebras\" (arXiv:2607.25249). In a single Lean source, the development kernel-checks the paper-local deductive architecture used for the new maximal-ideal cases: affine-kernel detection and lifting, extremal PBW-line deductions, finite Ramond--Casimir arithmetic and case enumerations, reduced-simplicity contradiction schemes, and the case-level affine conclusions for the level -1 D_l family and the positive-parameter cases of D4, E6, E7, and E8. It also audits…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-08-23","reactions":{}}