💻 computer science

Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4

This paper introduces Prismriver, a Lean 4 library that formalizes music theory to enable verifiable algorithmic composition, generalize beyond equal temperament tuning, model counterpoint, and interoperate with standard music software via a custom DSL and MusicXML exports.

Original authors: Leni Aniva, Claire Wang

Published 2026-07-14

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Leni Aniva, Claire Wang

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine music theory not as a dusty rulebook of "do this, don't do that," but as a giant, invisible playground of mathematical shapes. For centuries, musicians have played by these shapes intuitively, but they've never been able to build a robot that could prove the shapes were perfect. That's where Prismriver comes in. It's a new digital toolbox built inside a super-smart computer program called Lean 4, designed to turn music theory into a game of verifiable logic.

Think of Prismriver as a universal translator for music. Before this, most computer music tools assumed the world only had one way to tune instruments: the standard "equal temperament" (the 12 notes you find on a piano). It's like assuming every language in the world only has 26 letters. Prismriver breaks that rule. It allows you to invent any scale you want, even ones with "quarter-tones" (tiny notes between the piano keys) or scales where the "octave" isn't the main repeating pattern. It's like giving a composer a keyboard where the keys can stretch, shrink, or disappear, and the computer can still understand the math behind it.

The "Proof" Playground

The coolest part of Prismriver is how it treats music rules. Usually, if a composer writes a song, we just listen to it and say, "Yeah, that sounds good." But with Prismriver, you can write a song and ask the computer to prove it follows the rules.

Imagine you are building a tower of blocks. In the old days, you'd just stack them and hope they don't fall. With Prismriver, you have a magical inspector that checks every single block placement against the laws of physics before you even drop the next one. If you try to put a "dissonant" block (a clashing note) where a "consonant" one (a harmonious note) is required, the computer doesn't just say "oops"; it stops you and says, "This proof is incomplete."

The authors used this to tackle counterpoint, an ancient art of weaving two or more melodies together. They wrote a set of strict rules for "First Species Counterpoint" (a specific, beginner-friendly style of weaving melodies). They didn't just write code to make the music; they wrote code to prove the music they made followed the rules. It's like writing a story where the plot holes are mathematically impossible to exist.

The "Time Travel" Clock

Music happens in time, and Prismriver has a clever way of handling it. Instead of counting every single beat from the start of the universe (which gets messy), Prismriver uses a "bar and offset" system. Think of it like a subway map: you know which station (bar) you are at, and how far down the platform (offset) you are. This makes it super easy to shift a whole song forward or backward without recalculating every single second. It also allows for "negative offsets," which is like having a musical pickup note that starts before the official downbeat, a trick composers love.

The "Lego" Language

To make this accessible, Prismriver includes a special language that looks a lot like LilyPond, a text-based way to write music. You can type something like c'4 (a C note in a specific octave) and the computer understands it instantly. But here's the kicker: Prismriver can take your text, check your math, and then export the result into a universal file format called MusicXML. This means you can compose a song in this high-tech math language, prove it's perfect, and then open it in standard music software like MuseScore or LilyPond to play it on a real instrument. It's like building a spaceship in a video game, proving the engine works, and then exporting the blueprints to a real factory.

What It's NOT (and What It's Not Yet)

It's important to know what Prismriver doesn't do, so we don't get our hopes up too high.

It's not a magic song generator: The paper doesn't claim Prismriver can write a hit song on its own. It's a tool for algorithmic composition, meaning it helps you write the rules for a song, but you (or a specific algorithm you design) still have to decide the melody.
It doesn't do visuals yet: While it can play music, the paper explicitly states that generating visual art to go with the music is "subject to future work." So, no dancing lasers just yet.
It's not limited to Western music: While it handles Western classical music beautifully, the authors are careful to say it's designed to be flexible enough for "xenharmonic" (non-standard) scales, like the Bohlen-Pierce scale where the main repeating interval is a "tritave" (a 3:1 frequency ratio) instead of an octave.

The Bottom Line

Prismriver is a formalization library. This is a fancy way of saying it's a collection of verified math tools for music. The authors have successfully proven that the old-school "dihedral group" math (a complex way of describing how chords rotate and flip) works perfectly for standard 12-tone music, and they've generalized it to work for any tuning system you can imagine.

They haven't solved the mystery of "what makes a song beautiful," but they have built a proof-checker for music theory. If you want to compose a song where every single note is mathematically guaranteed to follow the rules of counterpoint, Prismriver is the first tool that can actually say, "Yes, I have checked the math, and this song is valid." It turns music composition from a game of guess-and-check into a game of verified logic, opening the door for a future where computers can help us compose music that is not just heard, but proven.

Technical Summary: Prismriver

Problem Statement

Music theory is governed by a rich set of mathematical rules and symmetries that can be expressed in precise mathematical language. However, traditional mathematical music theory relies on natural language proofs, which are subject to human error, lack mechanical verification, and do not allow for the reuse of results in a computational context. While previous formalizations of music theory exist, many are limited to specific tuning systems (such as 12-tone equal temperament) or lack the ability to perform algorithmic composition and analysis within a unified framework. There is a need for a formalization that supports arbitrary tuning systems, allows for machine-verified proofs of musical properties, and integrates these proofs with algorithmic composition and input/output capabilities.

Methodology

The authors present Prismriver, a formalization library for music theory and algorithmic composition built in Lean 4. Lean serves as both a functional programming language and an interactive theorem prover, enabling the library to define musical structures, prove theorems about them, and generate music.

Core Representations

Abstract Scales and Tuning:
- Prismriver defines a PseudoScale as a generic pitch type $P$ without restrictions, allowing for representations like real-number frequencies.
- A Scale is defined as a pitch type $P$ equipped with an interval type $I$ , where $I$ forms an abelian additive group acting on $P$ (an $I$ -torsor). This generalizes the concept of pitch classes beyond the standard 12-tone system.
- Xenharmonic Support: The library accommodates non-equal temperament tuning, quartertones, and scales with fundamental intervals other than the octave (e.g., the Bohlen-Pierce scale with a tritave). It distinguishes between enharmonic pitches (e.g., $C\sharp$ vs. $D\flat$ ) even if they are acoustically equivalent in 12-tone equal temperament, which is crucial for analyzing non-equal tempered systems like Pythagorean tuning.
Time and Notes:
- Time is modeled as an ordered abelian additive group $T$ .
- A note is defined as a pair $(P, T)$ , consisting of a pitch and a duration.
- A MeasuredTime type is implemented as a product of an integer (bar number) and a rational number (offset within the bar), facilitating analysis of pickups and shifting music without recalculating total beat counts.
Transpose Actions and Dihedral Groups:
- The library generalizes the concept of transposition and inversion. It defines a TransposeAction which includes translation ( $r_i$ ) and reflection ( $sr_{a,i}$ ) operations acting on arbitrary scales.
- The authors prove that under 12-tone equal temperament, these generalized transpose actions are equivalent to the action of the dihedral group $D_{12}$ on triads. This bridges the gap between abstract group theory and specific Western music theory models found in prior literature (e.g., [19]).
Monadic Composition:
- Algorithmic composition is handled via a CompositionT monad. This monad tracks a "current time" cursor and provides primitives to move the cursor, add events (articulations), and add notes.
- A Score.foldlM monad allows for the analysis of scores by folding over lists of ongoing events.
- These monadic structures enable the verification of composition algorithms (e.g., proving that a generated counterpoint adheres to specific rules) using Lean's LawfulMonad class.
Input/Output:
- DSL: A LilyPond-like Domain Specific Language (DSL) allows users to input music using text-based syntax. The DSL uses fixed pitch notation rather than relative notation to reduce volatility.
- Export: Scores are exported to MusicXML (time-wise format, converted to part-wise for compatibility with tools like LilyPond and MuseScore).
- Playback: The #play directive elaborates expressions and spawns an Alda process for interactive playback.

Key Contributions

Formalization of Music Theory: A comprehensive library formalizing pitches, accidentals, scales, chords, durations, and parts in Lean 4.
Generalized Tuning Compatibility: Support for xenharmonic scales, including non-equal temperament systems and scales with fundamental intervals other than the octave, moving beyond the limitations of 12-tone equal temperament.
Provable Reduction: A formal proof demonstrating that under 12-tone equal temperament, the generalized transpose action is equivalent to the $D_{12}$ dihedral group action on triads.
Monadic Algorithmic Composition: A framework for composing and analyzing music using monadic primitives, allowing for the verification of composition algorithms (e.g., first species counterpoint).
Interoperability: Integration of a custom DSL for music input and MusicXML export for compatibility with external music software, alongside direct playback via Alda.

Results and Implementation

The paper demonstrates the utility of Prismriver through several implementations:

Counterpoint Composition: The authors implemented a subset of first species counterpoint rules. They defined predicates for harmonic and melodic intervals, consonance, and specific constraints (e.g., no tritone turning points). Using these predicates, they constructed counterpoint programmatically and proved that the resulting compositions satisfy the rules of first species counterpoint.
Chord Progression Analysis: The library was used to analyze the chord progression of Pachelbel's Canon in D in terms of transpose actions and chord inversions, validating the generalized dihedral action model.
Code Examples: The paper includes code snippets showing the definition of intervals, the implementation of the dihedral group action on triads, and the use of the composition monad to generate a melody (based on Necrofantasia).

Significance

The paper claims that Prismriver opens the door to verifiable algorithmic composition and accompaniment generation. By formalizing music theory in a proof assistant, the authors enable:

Mechanical Verification: Errors in musical proofs can be detected by the computer, eliminating the inefficiencies of handwritten proofs.
Reusability: Results and primitives can be mechanically reused in future proofs and compositions.
Flexibility: The library allows users to define custom tuning systems and musical primitives, fostering a growing, reusable library of music formalization.
Integration: It bridges the gap between theoretical music analysis and practical composition tools, allowing for the generation of MusicXML that can be played by standard software.

The authors position Prismriver as a step beyond existing tools like Lulu (which lacks generalized tuning primitives) and HarmTrace or Mezzo (which are limited to specific type-system encodings or tuning systems). By leveraging Lean's expressive power, Prismriver provides a versatile environment where music theory can be both proven and executed.