formalizing music theory

Stream: lean4

[Arthur Paulino]

I'm having some fun formalizing Music Theory in Lean 4 :smiley:
If you're interested: https://github.com/arthurpaulino/LeanMusic

[Kyle Miller]

Maybe this is already what you're thinking, but one goal you could have that's in that general direction is to formalize so-called "musical set theory" (that's the theory of musical sets, by the way, not set theory that's musical). There are something you could prove about properties of different sets of pitch classes and how they're acted upon by the group generated by inversion and transposition. You can do the same with tone rows (permutations of the 12 pitch classes), but its group has other operations reversing the pitches in time.

[Kyle Miller]

This is only part of the theory for some specific kinds of 20th century music, but it seems particularly well-suited for formalization.

[Arthur Paulino]

I'm definitely going to check that out. But from what you described, it's very similar to what I have in mind. I want to have some results about equivalence of scales, definition of chords and their inversions, harmonic fields and their relationships with chords.
I also want to reach the point of proving that, for instance, every M7+ chord is in two different harmonic fields etc. This is for melody/harmony.

There's also an entertaining amount of arithmetic involved in rhythm and bar signatures. But I will think about it later

[Kyle Miller]

Musical set theory doesn't care too much about triadic harmony, but it can't hurt developing it for all the different equivalences.

If you also do "pointed musical sets," which is some math-inspired terminology I just made up for a musical set along with a chosen pitch class in it, then you can use that chosen pitch class as the root of the chord, which is important for chord identification.

[Arthur Paulino]

Do you have some references on musical set theory?

[Arthur Paulino]

There are some places where I hardcoded "12". I can see how this theory can be generalized for any amount of different pitches

[Kyle Miller]

You're formalizing 12 EDO (equal division of the octave). Here is one possible entry point into alternative scales: https://en.xen.wiki/w/Main_Page (the xenharmonic wiki)

[Kyle Miller]

(For example, 53 EDO has a better approximation of the 3/2 frequency ratio (a perfect fifth) than 12 EDO, and it has a good, if a bit flat, 5/4 ratio (a just major third). I believe Newton noticed this when studying convergents of logarithms, though he wasn't the first.)

[Arthur Paulino]

Mother god, by seeing the impossibility to prove a theorem I was able to notice a bug in a function that I wasn't able to catch with tests :open_mouth: