Mathematical Proofs as Music: Metamath Music

This is a fun thing. For more about the underlying system, see: http://us.metamath.org/mpeuni/mmset.html

Reminds me of an old Rudy Rucker story, 'A New Golden Age':

Listening to "axiom of choice equivalent" there is at some point a descending line and then a repetition of the main theme. Quite interesting.

You can play the .mid files with VLC media player.

My VLC says these files (the ones I got, anyway) are in the wrong format to be played and it throws an error.

You can otherwise try opening it in musescore, that worked for me too: https://musescore.org/en