Presents Prismriver, a Lean 4 library formalizing music theory with Mathlib group actions and supporting verifiable algorithmic composition.
Abstract
Music theory obeys a rich set of mathematical rules and symmetries. These symmetries follow mathematical structure which can be verified and expressioned in the precise language of a proof assistant. In this paper, we present Prismriver, a formalization of music theory in Lean 4. By formalizing music theory in Lean 4, we open the door to verifiable algorithmic composition and accompaniment generation. We also enable the analysis of monadic analysis of structures in music.
Problem
Music theory obeys mathematical rules and symmetries that a proof assistant could verify, but no Lean library represented music for analysis and composition.
Approach
Prismriver models pitch as a torsor over an interval group using Mathlib group actions, accommodating tuning systems beyond equal temperament. It provides a Lilypond-like DSL and a #play directive backed by the Alda language, plus a monadic CompositionT interface and a score-analysis fold for algorithmic composition and accompaniment, with composition algorithms reasoned about via Lean's LawfulMonad.
Figure 2. Lattice formed by major third i_{\mathsf{M3}} and minor third i_{\mathsf{m3}}
Results
A Lean 4 library compatible with Mathlib, Alda, MIDI, and MusicXML that supports representation, analysis, and algorithmic composition of music.
Figure 3. Chord progression of Pachelbel, Canon in D, analyzed in terms of transpose actions
