Mathematical Proofs as Music: Metamath Music

Click on a theorem name to see its proof, and click on the musical note to hear it set to music. To create the MIDI file for theorem , open an MS-DOS or Command Prompt window (Start -> Programs -> Accessories -> Command Prompt, or Start -> Run -> command, or Start -> Run -> cmd) and type:

The parameter argument is specified by a combination of the following letters, with no spaces separating them:

You can see what theorems are available by typing ” “. So in this example the midi note numbers will be be

    where 53 = 65-12 is the shifted note of step 11, which you can see has a in it in the proof listing.

Source: us.metamath.org