This August we're hosting Claire Wang to present Prismriver, a formalization of music theory and algorithmic composition in Lean 4, developed jointly with Leni Aniva. The paper opens with the observation that music is, at heart, a mathematical object:
Music theory obeys a rich set of mathematical rules and symmetries. These symmetries follow mathematical structure which can be verified and expressed in the precise language of a proof assistant.
By encoding the rules of music theory as Lean definitions and theorems, Prismriver makes those rules machine-checkable rather than merely conventional. That foundation opens the door to verifiable algorithmic composition and accompaniment generation, where a generated piece can be checked against the formal structure it claims to respect, and it enables a monadic analysis of the structures that recur throughout music.
Prismriver is built as a music DSL in Lean 4; the source lives in the project's GitHub repository. Come hear Claire walk through the formalization and where it leads next at her talk on Sunday, August 16.