pith. sign in

arxiv: 2606.19936 · v1 · pith:WMJFFCHFnew · submitted 2026-06-18 · 💻 cs.LO · cs.MM

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

Leni Aniva , Claire Wang This is my paper

Pith reviewed 2026-06-26 15:26 UTC · model grok-4.3

classification 💻 cs.LO cs.MM
keywords music theoryLean 4formalizationalgorithmic compositionproof assistantmonadic structuresverification
0
0 comments X

The pith

Formalizing music theory in Lean 4 enables verifiable algorithmic composition and monadic analysis of musical structures.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Prismriver, a formalization of music theory in Lean 4. It claims that this encoding of mathematical rules and symmetries in a proof assistant opens the door to verifiable algorithmic composition and accompaniment generation. The work also enables formal analysis of monadic structures in music. A reader would care if the formalization succeeds because it applies precise verification techniques to a domain traditionally handled by informal rules.

Core claim

Prismriver is 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.

What carries the argument

Prismriver, the Lean 4 formalization that encodes the mathematical rules and symmetries of music theory.

If this is right

  • Algorithmic compositions can be checked for adherence to music theory rules inside the formalization.
  • Accompaniment generation can be produced with formal verification guarantees.
  • Monadic structures appearing in music can be analyzed using Lean 4 tactics and proofs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same formalization approach could be extended to verify larger-scale musical forms such as full pieces rather than isolated phrases.
  • Integration with other Lean libraries for mathematics might allow cross-domain proofs linking music to geometry or group theory.
  • If the formalization is expressive enough, it could serve as a basis for certified music education tools that prove correctness of student exercises.

Load-bearing premise

The mathematical rules and symmetries of music theory can be captured in Lean 4 with sufficient fidelity to support non-trivial algorithmic composition and analysis.

What would settle it

An example of a non-trivial algorithmic composition or accompaniment that follows standard music theory yet cannot be verified or analyzed inside the Prismriver formalization.

Figures

Figures reproduced from arXiv: 2606.19936 by Claire Wang, Leni Aniva.

Figure 1
Figure 1. Figure 1: Action of augmented fourth 𝑖A4 and diminished fifth 𝑖D5 on classical pitches. The combination of them pro￾duces a diminished second, which relates enharmonic notes. 𝐵3 𝐶4 𝐷4 𝐸4 𝐹4 𝐺4 𝐴4 𝐵4 𝐶5 𝐷5 𝄫 ♭ ♮ ♯ 𝄪 [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Lattice formed by major third 𝑖M3 and minor third 𝑖m3 tuning system. A corner stone of music theory is the concept of chords and chord progressions, where music moves from chord to chord. A method to model chord progressions is via dihedral actions [7], where a dihedral action on the circle of fifths maps one chord to another chord. Pitch classes are represented as elements of Z12, while transpositions and… view at source ↗
Figure 3
Figure 3. Figure 3: Chord progression of Pachelbel, Canon in D, ana￾lyzed in terms of transpose actions while an inversion is represented by a reflection followed by a rotation, 𝑠𝑟𝑖 (𝑝) = −𝑝 + 𝑖 (mod 12). inductive Parity : Type | major | minor deriving DecidableEq, Repr, Fintype -- We use parity to describe whether a chord is major or minor. -- When we invert a chord, its parity flips. def Parity.flip : Parity → Parity | .ma… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 2 minor

Summary. The paper presents Prismriver, a formalization of music theory in Lean 4. It claims that formalizing the mathematical rules and symmetries of music theory in a proof assistant opens the door to verifiable algorithmic composition, accompaniment generation, and monadic analysis of musical structures.

Significance. A substantial, machine-checked formalization of music theory could provide a foundation for verified composition tools. However, the manuscript contains no definitions, theorems, code, or examples, so it is impossible to determine whether any such contribution has been made.

major comments (1)
  1. Abstract: The abstract provides no definitions, theorems, or examples; therefore no assessment of whether the formalization actually supports the stated claims is possible.
minor comments (2)
  1. Abstract: 'expressioned' is not standard English; 'expressed' is the intended term.
  2. Abstract: The phrase 'monadic analysis of structures in music' is vague and requires clarification or an example.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for their review. We agree that the abstract as written provides insufficient detail to evaluate the claims and will revise it substantially.

read point-by-point responses

  1. Referee: Abstract: The abstract provides no definitions, theorems, or examples; therefore no assessment of whether the formalization actually supports the stated claims is possible.

    Authors: We agree that the submitted abstract lacks concrete definitions, theorems, or examples. The full manuscript body presents the Lean 4 formalization of music-theoretic structures (e.g., pitch classes as elements of Z/12Z, interval addition as a group operation, and verified closure properties for diatonic scales), but these were not summarized in the abstract. We will expand the abstract to include at least one key definition (e.g., the type of a musical note) and one theorem (e.g., transposition invariance of the major scale) along with a brief code snippet. revision: yes

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper is a direct formalization of existing music theory concepts into Lean 4, with no derivation chain, equations, fitted parameters, predictions, or load-bearing self-citations. The claim that formalization 'opens the door' to verifiable composition follows immediately from the act of formalization in a proof assistant and does not reduce to any unverified input or self-referential definition. No patterns of self-definition, fitted-input-as-prediction, or ansatz smuggling appear. The work is self-contained against external benchmarks of formalization projects.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the domain assumption that music theory consists of formalizable mathematical rules and on the standard assumption that Lean 4's type theory is adequate for the encoding. No free parameters or invented entities are visible in the abstract.

axioms (2)
  • standard math Lean 4's dependent type theory is sound for encoding mathematical structures
    Invoked implicitly by any Lean formalization project.
  • domain assumption Music theory obeys a rich set of mathematical rules and symmetries that can be expressed in a proof assistant
    Stated in the first sentence of the abstract as the premise for the entire effort.

pith-pipeline@v0.9.1-grok · 5592 in / 1207 out tokens · 14911 ms · 2026-06-26T15:26:53.105908+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

17 extracted references · 7 canonical work pages · 1 internal anchor

  1. [1]

    Getting Started Strudel.https://strudel.cc/workshop/getting- started/

    2026. Getting Started Strudel.https://strudel.cc/workshop/getting- started/

    2026

  2. [2]

    Live code with Tidal Cycles | Tidal Cycles.https://tidalcycles.org/

    2026. Live code with Tidal Cycles | Tidal Cycles.https://tidalcycles.org/

    2026

  3. [3]

    Mathematics in Mathlib.https://leanprover-community.github

    2026. Mathematics in Mathlib.https://leanprover-community.github. io/mathlib-overview.html

    2026

  4. [4]

    Mathlib.Algebra.Group.Action.Basic.https://leanprover- community.github.io/mathlib4_docs/Mathlib/Algebra/Group/ Action/Basic.html

    2026. Mathlib.Algebra.Group.Action.Basic.https://leanprover- community.github.io/mathlib4_docs/Mathlib/Algebra/Group/ Action/Basic.html

    2026

  5. [5]

    MusicXML for Exchanging Digital Sheet Music.https://www

    2026. MusicXML for Exchanging Digital Sheet Music.https://www. musicxml.com/

    2026

  6. [6]

    Youyou Cong. 2023. Weighted Refinement Types for Counterpoint Composition | Proceedings of the 11th ACM SIGPLAN International Workshop on Functional Art, Music, Modelling, and Design.https: //dl.acm.org/doi/10.1145/3609023.3609804

    work page doi:10.1145/3609023.3609804 2023

  7. [7]

    Musical Actions of Dihedral Groups

    Alissa S. Crans, Thomas M. Fiore, and Ramon Satyendra. 2008. Musical Actions of Dihedral Groups. doi:10.48550/arXiv.0711.1873 arXiv:0711.1873 [math.GR]

    work page internal anchor Pith review Pith/arXiv arXiv doi:10.48550/arxiv.0711.1873 2008

  8. [8]

    Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language | Springer Nature Link.https: //link.springer.com/chapter/10.1007/978-3-030-79876-5_37

    work page doi:10.1007/978-3-030-79876-5_37 2021

  9. [9]

    Dave Yarwood et al. 2026. Alda: A music programming language for musicians.https://github.com/alda-lang/alda

    2026

  10. [10]

    Mark Gotham and Kris Shaffer. 2021. First-Species Counterpoint. (July 2021).https://viva.pressbooks.pub/openmusictheory/chapter/first- species-counterpoint/Book Title: Open Music Theory

    2021

  11. [11]

    John Harrison, Josef Urban, and Freek Wiedijk. 2014. History of Interactive Theorem Proving. InHandbook of the History of Logic. Vol. 9. Elsevier, 135–214. doi:10.1016/B978-0-444-51624-4.50004-6

    work page doi:10.1016/b978-0-444-51624-4.50004-6 2014

  12. [12]

    2026.First Species Counterpoint.https:// musictheory.pugetsound.edu/mt21c/FirstSpecies.html

    Robert Hutchinson. 2026.First Species Counterpoint.https:// musictheory.pugetsound.edu/mt21c/FirstSpecies.html

    2026

  13. [13]

    Ranjit Jhala and Niki Vazou. 2020. Refinement Types: A Tutorial. doi:10.48550/arXiv.2010.07763arXiv:2010.07763 [cs.PL]

    work page doi:10.48550/arxiv.2010.07763arxiv:2010.07763 2020

  14. [14]

    Gareth Loy and Curtis Abbott. 1985. Programming languages for com- puter music synthesis, performance, and composition.ACM Comput. Surv.17, 2 (June 1985), 235–265. doi:10.1145/4468.4485

    work page doi:10.1145/4468.4485 1985

  15. [15]

    Click Nilson. 2007. Live coding practice. InProceedings of the 7th international conference on New interfaces for musical expression (NIME ’07). Association for Computing Machinery, New York, NY, USA, 112–

    2007

  16. [16]

    doi:10.1145/1279740.1279760

    work page doi:10.1145/1279740.1279760

  17. [17]

    Palalansoukî. 2026. iehality/Lulu.https://github.com/iehality/Lulu original-date: 2025-01-10T15:12:19Z

    2026