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.