From the Metamath Music page:
"While looking at some proofs, it occurred to me that their structure resembled musical scores, so as an experiment I decided to see what they sounded like. Essentially, the musical notes correspond to the depth of the proof tree as the proof is constructed by the proof verifier. A fast higher note is produced for each step in the construction of a formula."
You can hear the music here:
Some mathematical musical mock-ups include: Law of identity, Russell's paradox, Peirce's axiom MIDI, Praeclarum theorema, Proposition *5.18 from Principia Mathematica, Function value in terms of ordered pair, Cantor's theorem, The existence of omega, Transfinite induction, Transfinite recursion, Schröder-Bernstein Theore, Pigeonhole Principle, Axiom of Choice equivalent, Zermelo's well-ordering theorem, and others.
The music is faithful to the original theorems and proofs. For example, the five sustained (lower) notes you will hear in the Law of Identity match, in order, the five steps of its proof, while the faster notes represent the construction of the formulas used in those steps.
"Is it "music"? I guess that's for you to decide. It is richly structured, with underlying themes that on the one hand seem to repeat but on the other hand are interestingly unpredictable, teasing your mind as the piece progresses."