[FARM'26] Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4

Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4 (Video, FARM 2026) Leni Aniva, Claire Wang (Stanford University, USA; University of Pennsylvania, USA) Abstract: Music theory obeys a rich set of mathematical rules and symmetries. These symmetries follow mathematical structures which can be verified and expressed in the precise language of a proof assistant. In this paper, we present Prismriver, a formalization library of music theory in Lean 4. We use Prismriver to generalize beyond existing work that assumes equal temperament tuning. We also discuss modelling counterpoint music theory with Prismriver. By formalizing music theory in Lean 4, we open the door to verifiable algorithmic composition and accompaniment generation. Prismriver also has a custom DSL integrated with MusicXML exports to interoperate with other music software. Prismriver can be used to compose music with Lean, using monadic composition primitives. Article: https://doi.org/10.1145/3830435.3830954 ORCID: https://orcid.org/0000-0002-6033-9140, https://orcid.org/0009-0002-9321-0877 Video Tags: Music Theory, Music, Lean 4, Algorithmic Composition, doi:10.1145/3830435.3830954, orcid:0000-0002-6033-9140, orcid:0009-0002-9321-0877 Presentation at the FARM 2026 workshop, August 24, 2026, https://icfp26.sigplan.org/home/farm-2026 Sponsored by ACM SIGPLAN.