Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4
Abstract
Prismriver is a Lean 4 library that formalizes music theory with generalized tuning and counterpoint rules to enable verifiable algorithmic composition and software interoperability.
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.
Get this paper in your agent:
hf papers read 2606.19936 Don't have the latest CLI?
curl -LsSf https://hf.co/cli/install.sh | bash Models citing this paper 0
No model linking this paper
Datasets citing this paper 1
Spaces citing this paper 0
No Space linking this paper
Collections including this paper 0
No Collection including this paper