Prismriver: Formalization of Music Theory and Algorithmic Composition in Lean 4
summary
Prismriver is a Lean 4 library that formalizes pitches, intervals and scales as group actions, proves dihedral-action equivalences (triads on Z12 vs a non-modular 2D pitch model), and generalizes beyond equal temperament to arbitrary tuning systems; it stores pitches as a name plus semitone so C# ≠ Db formally, proves interval-addition laws, encodes 0‑4‑7 triads and dihedral transforms, offers a LilyPond‑style DSL with MusicXML export, and provides a monadic composition API supporting randomness and verified counterpoint propositions.
AI-written summary · about
chapters (9)
- 0:00Prismriver project intro
- 2:29Library overview and features
- 4:37Music theory in Lean 4
- 9:27Pitches, intervals, tuning
- 11:15Dihedral group on triads
- 13:24Input/output and music DSL
- 14:49Algorithmic composition
- 15:51Counterpoint case studies
- 19:25Q&A: Extensions and Bach
related talks
32mScala, Sound, and Structure - Composing Music through FP
33mWriting Music with Ruby: A subtle introduction to music theory
23mGirard's Paradox as Structure Music
19mComposing music with composed functions
51mMaking Music with Ruby: Patterns, Context, Fun
32mI wrote a Ruby Library to help me compose my music album
45mSongwriting in Scala: Creating a DSL for writing Music with ADT's
25mDemo: Composable Compositions in Tonart