I went looking for formalisations of counterpoint specifically, and stumbled on this paper about formalising music theory in general using Lean. FugueBench here I come arxiv.org/abs/2606.19936
Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4
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...
arxiv.org