Metamath Music Page

Contents of this page Mathematical Proofs Set to Music Music Sampler Music Visualization How to Generate this Music The Algorithm Experimenting With the Algorithm An Original Arrangement Copyright Considerations

The Metamath Music Page offers some eerie sounds that will certainly pass for music in avant-garde circles. We must admit to a certain fascination at hearing the steps of a proof rendered as notes that occasionally announce themes, only to abandon them. — AK Dewdney (author, The Turing Omnibus) Metamath Music Page - Proofs you can listen to in MIDI format. Fun and edjemacational! — Haddon Kime (composer, music score for the play Proof) ...instead of turning in analysis homework, I'll just bring an electronic piano to class and play the proof for my professor. — User MarcME222, digg.com

Mathematical Proofs Set to Music    I added this web page just for fun. 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. A sustained lower note is produced when the formula is matched to a previous theorem or earlier proof step, to result in a new proof step (which corresponds to a proof step displayed on the Metamath Proof Explorer page that shows the theorem's proof).

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.

For these MIDI files, make sure your media player is set to a "piano" sound and not an "electronic organ" sound, otherwise it will sound horrible, because the sustained notes need to decay automatically. For example, I had to select Yamaha OPL3-SA SoftSynth from Devices/Properties in Microsoft Media Player on a Windows 95 computer I tried. More recent computers seem to default to the piano sound. If you are using QuickTime, it has a bug that sometimes causes a burst of loud, annoying static at the beginning of a piece; you can work around this bug by changing the MIDI settings [retrieved 3-Feb-2017 from archive.org].

I set the tempo quite fast, partly to help you decide more quickly whether it interests you. (The tempo can be slowed down by rerunning the program that generated these.) I chose to give the selections a "syncopated" character by substituting a repeated note with a silent pause, since to me it usually sounded a little better. The frenetic non-syncopated version can be interesting too, with one note for every proof step. Sometimes, syncopation has only a small effect, as in the case of the Second Peano Postulate 0:16. Other times the effect is significant; compare the syncopated1:49 and non-syncopated1:49 versions of the Triangle Inequality (and also another version). Another curious piece with a pronounced syncopated effect is the Square Root Theorem 0:41.

In deeper proofs, a kind of tension sometimes builds up, with occasional partial relief but growing overall, until finally many subproofs come together. For example, you may want to sample the Axiom of Choice Equivalent 3:51, where a crescendo slowly builds up starting at around 2:20 minutes, reaching a dramatic climax at 3:11 minutes and then suddenly cascading down to the main theme. Another frenzied, climactic piece is Zermelo's Well-Ordering Theorem 0:50. The Schröder-Bernstein Theorem 1:47 (I like this one) changes its theme during its course, starting off with a ominous staccato then breaking out into a colorful display of notes.

The music generated from these mathematical proofs stands in sharp contrast to certain other experimental music based on such mathematics as the digits of π (pi). Unlike a proof's tree structure, which is inherently suggestive of a musical score, the digits of π have no obvious pattern. To make it interesting, a human composer will often add a non-mathematical creative element such as an underlying beat with pre-selected chords and instrumentation. What one hears, then, might be based as much on the originality of the composer as on the essential nature of π: the same algorithm applied to the digits of say e (Euler's constant), or even a series of random digits, would typically sound about the same after the first few notes. The music here, on the other hand, is a raw and unadorned representation of the mathematics itself, involving few human preconceptions beyond a basic mapping needed to accommodate the Western tonal scale.

Music Sampler   

The theorems below are from (the August 2000 version of) the Theorem Sampler on the Metamath Proof Explorer Home Page. Click on a theorem name to see its proof, and click on the musical note to hear it set to music. The music is faithful to the original 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.

Law of identity 0:05 Peirce's axiom 0:03 Praeclarum theorema 0:06 Proposition *5.18 from Principia Mathematica 0:47 Existential quantifier introduction 0:10 x = x 0:10 Existential elimination by uniqueness 0:03 Basic relationship between class and wff variables 0:10 Two ways of saying "is a set" 0:06 Derivation of Separation Axiom 0:41 Derivation of Empty Set Axiom 0:02 Derivation of Pairing Axiom 1:30 Subset defined in terms of set difference 0:32 Russell's paradox 0:20 Associativity of function composition 1:41 Function value in terms of ordered pair 0:06 Cantor's theorem 1:27 Mathematical induction 0:14 Peano's postulates: 1 0:06 2 0:16 3 0:01 4 0:35 5 3:39

The existence of omega 0:20 Transfinite induction 1:19 Transfinite recursion 0:18 Schröder-Bernstein Theorem 1:47 Pigeonhole Principle 2:35 Axiom of Choice equivalent 3:51 Zermelo's well-ordering theorem 0:50 Zorn's Lemma 5:05 The 27 postulates for real and complex numbers: 1 0:01 2 0:06 3 0:02 4 0:06 5 0:51 6 0:27 7 1:34 8 0:27 9 0:09 10 0:34 11 0:39 12 6:46 13 3:37 14 0:06 15 0:34 16 1:13 17 2:16 18 7:45 19 1:20 20 1:45 21 1:14 22 0:04 23 0:04 24 1:59 25 1:17 26 3:11 27 4:37 Archimedean property of real numbers 0:58 Square root theorem 0:41 Complex number in terms of real and imaginary parts 0:02 Complex conjugate 0:12 Triangle inequality for absolute value 1:49 2 + 2 = 4 for complex numbers 0:07

Each of the above proofs is actually just the highest level of each theorem's proof, where typically several other theorems are pieced together to obtain the final result. In fact the Metamath database has over 7,000 other proofs - who knows what they sound like!

Music Visualization    It is interesting to look at the visualizations of music structure that are produced by Martin Wattenberg's The Shape of Song [retrieved 3-Feb-2017] Java applet. At the top we show the Schröder-Bernstein Theorem 1:47. Under it we show the theme song for the TV show Futurama and Beethoven's Sonata Pathetique, Adagio.

Schröder-Bernstein Theorem visualization
Futurama visualization	Sonata Pathetique visualization

What does this mean? I'm not sure, other than that it says something about the complexity of the music structure. But it looks neat. [Images used by permission of Martin Wattenberg.]

How to Generate this Music    (Note added 28-Nov-2002:  The MIDI files here were created in Aug. 2000, and shorter proofs have since been discovered for some of the theorems. This means the MIDI files generated from the current database may not always be the same as the ones on this page. Contact me if you would like the old set.mm database that reproduces exactly the results on this page.)

Here is how to generate these melodies with the Metamath program. There are currently over 19,000 proofs in the Metamath database set.mm, each with a different melody.

For Windows:
Step 1. Extract the file t2mf.exe (a program that converts a text file to a MIDI file) from mf2t.zip, which you can download from http://www.hitsquad.com/smm/programs/mf2t/download.shtml [retrieved 3-Feb-2017]. (You can also download and unzip mf2t.zip. The t2mf.exe file is located in the folder mf2t\mf2t-original\mf2t\.)

Step 2. Extract the files metamath.exe (the Metamath program) and set.mm (the Metamath set theory database) from metamath.zip, which is the Metamath Program download.

Step 3. Put the three files metamath.exe, set.mm and t2mf.exe into a new directory (folder).

Step 4. Browse through the Metamath Proof Explorer proof pages to find a proof you want to listen to. For this example, we'll suppose you want to listen to the Schröder-Bernstein Theorem, whose proof page is sbth.html. The name "sbth" is the name of the theorem that you will give to the program.

Step 5. Let's say you called your new directory C:\metamidi in Step 3. To create the MIDI file for theorem sbth, open an MS-DOS or Command Prompt window (Start -> Programs -> Accessories -> Command Prompt, or Start -> Run -> command, or Start -> Run -> cmd) and type:

  C:\WINDOWS>cd \metamidi
  C:\metamidi>metamath set.mm
  MM> midi sbth /parameter "fsh"
  Creating MIDI source file "sbth.txt"... length = 107 sec
  MM> exit
  C:\metamidi>t2mf sbth.txt sbth.mid

Now you can play the MIDI for the Schröder-Bernstein Theorem 1:47 by clicking on sbth.mid in the Windows Explorer.

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

• f = make the tempo fast (default is slow).
• m = make the tempo medium (default is slow). Both "f" and "m" should not be specified simultaneously.
• s = syncopate the melody by silencing repeated notes, using a method selected by whether the "h" parameter below is also present (default is no syncopation).
• h = allow syncopation to hesitate i.e. all notes in a sequence of repeated notes are silenced except the first (default is no hesitation, which means that every other note in a repeated sequence is silenced - this makes it sound slightly more rhythmic). The "h" parameter is meaningful only if the "s" parameter above is also present.
• w = use only the white keys on the piano keyboard (default is potentially to use all keys).
• b = use only the black keys on the piano keyboard (default is all keys). Both "w" and "b" should not be specified simultaneously.
• i = use an increment of one keyboard note per proof indentation level. The default is to use an automatic increment of up to four notes per level based on the dynamic range of the whole song. (An increment of "one keyboard note" means adjacent keys by default, successive black keys if "b" was selected, and successive white keys if "w" was selected.)

If you just type "midi sbth" and omit the parameter list, the defaults will be used. I used "midi sbth /parameter "fsh"" for the selections on this page.

You can see what theorems are available by typing "show labels". In general you can use "help" to guide you, including "help midi".

Tip:The "midi" command in Metamath will not destroy existing files, but will rename an existing one with ~1 appended (for example, an older sbth.txt would be renamed sbth.txt~1), an existing ~1 to ~2, etc. up to ~9. (An existing ~9 is deleted.) This makes it safer to use but also will clutter up your directory, so you may want to clean them out occasionally.

Tip: There is a problem with t2mf.exe: it can only handle Microsoft's 8.3 file format (8-character file name, period, and 3-character extension). It will complain if you ask it to convert pm2.11.txt because a file name can't have 2 periods, so you have to use the "real" Microsoft file name such as PM211~1.TXT which you can see with the MS-DOS DIR command (or DIR/X in the Windows XP Command Prompt). Alternately you could rename the file to, say, pm2_11.txt before running t2mf.exe. I am not the author of t2mf.exe and unfortunately have no other solution at this point.

MacOSX:
In 2006, Luca Ciciriello modified the program to run on MacOSX. Download and unzip mf2t.zip. The files are located in mf2t/mf2t-Mac/. I have not tested it personally.

For Unix/Linux:
The t2mf program was written in 1991, before C was standardized by ANSI, and it will not compile on modern compilers. However, if you wish to attempt to convert it to modern C, download and unzip mf2t.zip. The source files are located in mf2t/mf2t-original/mf2tsrc/, which includes the sources for t2mf. You may also wish to consult the sources for Luca Ciciriello's Mac upgrade, located in mf2t/mf2t-Mac/Midi_MacOSX_Xcode/Midi_MacOSX_Xcode/midisrc/t2mf/. If you are successful, let me know and I will add it to the mf2t.zip download. Note that the authors Tim Thompson (original author) and M. Czeiszperger agreed to place their code in the public domain, but I was unable to contact Piet van Oostrum who made some additional modifications to the code.

For Unix/Linux and MacOSX:
Assuming you have successfully compiled t2mf, next download the file metamath.tar.gz. Type:

  $ tar -xzf metamath.tar.gz

This will create a directory called "metamath". To compile the program with gcc, type

  $ cd metamath
  $ gcc m*.c -o metamath

Now you can run the Metamath program, then t2mf, to create the MIDI file:

  $ ./metamath
  MM> read "set.mm"
  MM> midi sbth /parameter "fsh"
  Creating MIDI source file "sbth.txt"... length = 107 sec
  MM> exit
  $ t2mf sbth.txt sbth.mid

See the notes above for Windows for information on the parameters.

The Algorithm    I'll use as an example the simple theorem idALT which is the Law of Identity 0:05. The database file set.mm stores the proof in a compressed format to save space, so first we must store it internally in uncompressed format, otherwise when we view the proof we'll see a more compact version with indirect references to repeated steps. (The "midi" command does the uncompressing automatically, but for "show proof" to show the format shown below, we must perform this step.) In the Metamath program, we type:

  MM> save proof idALT / normal

Then we type

  MM> show proof idALT / all

This will show the microsteps that construct wffs, as well as regular proof steps, in the form of an indented proof tree. The notation for proofs is described in the Metamath book (1.3Mb) if you are interested. You'll see:

   1     wph=wph   $f wff ph
   2       wph=wph   $f wff ph
   3       wps=wph   $f wff ph
   4     wps=wi    $a wff ( ph -> ph )
   5   wph=wi    $a wff ( ph -> ( ph -> ph ) )
   6     wph=wph   $f wff ph
   7     wps=wph   $f wff ph
   8   wps=wi    $a wff ( ph -> ph )
   9     wph=wph   $f wff ph
  10     wps=wph   $f wff ph
  11   min=ax-1  $a |- ( ph -> ( ph -> ph ) )
  12       wph=wph   $f wff ph
  13           wph=wph   $f wff ph
  14           wps=wph   $f wff ph
  15         wph=wi    $a wff ( ph -> ph )
  16         wps=wph   $f wff ph
  17       wps=wi    $a wff ( ( ph -> ph ) -> ph )
  18     wph=wi    $a wff ( ph -> ( ( ph -> ph ) -> ph ) )
  19         wph=wph   $f wff ph
  20           wph=wph   $f wff ph
  21           wps=wph   $f wff ph
  ...

Reading down, you can see the indentation levels (each level indents 2 more spaces) are successively
    2,3,3,2,1,2,2,1,2,2,1,3,...

We want to fit the proof within a desirable maximum dynamic range of note frequencies, which I defined as 27 < n < 104, where n is the midi note number. We obtain an the largest possible integer "scale factor", with a maximum of 4, that allows the music to fit in the dynamic range. For the idALT proof, the scale factor will be 4.

We also compute a "baseline" note which allows the proof to fit in the dynamic range. For the idALT proof, the baseline is 61.

We multiply the indentation level by the scale factor 4 and add it to the baseline. In addition, whenever we encounter a "logical" (real) proof step (as opposed to a formula-building proof step), identified by a |- in the proof listing, we shift the note down by 12 (one octave) and sustain it rather than turning it on and off.

So in this example the midi note numbers will be be
    69,73,73,69,65,69,73,65,69,69,53,73...
where 53 = 65-12 is the shifted note of step 11, which you can see has a |- in it in the proof listing.

Finally, if syncopation is selected, which was the case for all the selections on this page, repeated notes are replaced with silence. (The sustained notes are not syncopated.) So what we hear through step 12 above is
   69,73,-,69,65,69,-,65,69,-,53,73,...
where the 53 is the first sustained note.

Now, listen carefully to the Law of Identity 0:05, and you will hear that the first 12 notes and pauses match exactly the above sequence.

Experimenting With the Algorithm    If you know how to program in C, you can experiment with the algorithm. For example, you might want to try an alternative to the equidistant note algorithm, which not everyone likes:

"Kind of amusing in that the entire output of these pages proves a theorem of its own: that not all mathematicians make good music (take THAT, Douglas Hofstadter!). Mis-step one was to program using only equal distances between pitches (MIDI note numbers), resulting in endless whole-tone melodies." —musician Tom Djll [external]

(By the way, the "b", "w", and "i" parameters that are already available may appeal to more conventional musical tastes. An example is the Triangle Inequality 1:49 played with the black keys, using the parameter string "fsbi". To me it lacks some of the vaguely disturbing eeriness of the other versions, and there is a certain gentle pleasantness to it. What do you think?)

To modify the algorithm, download the Metamath program, which includes the source code. In the file mmcmds.c, at the very end you will find the function outputMidi() which generates the MIDI file. I put in a lot of comments, so hopefully you won't find it too hard to follow what it does. I recommend confining any experiments to this function, which gives you access to everything you should need. Let me know if there is something you don't understand.

Tip: In Metamath program download, the C programs are stored in Unix ASCII format with no carriage-return at the end of lines. If you are using Windows, see the note on text files at the end of the download help section.

The user parameter from the "/parameter" argument in the Metamath "midi" command is just an arbitrary string that is not syntax-checked, and you can use it to put in your own parameters to experiment with.

To compile the program, you need an ANSI C compiler such as gcc, which is built into Linux and available free for Windows as part of Cygwin [external]. Assuming you have only the Metamath source files in your directory, you type in the Cygwin or Linux shell

  gcc m*.c -o metamath.exe

where you omit the .exe in Unix/Linux.

An Original Arrangement    George Sherwood (old home page) has combined a few of the proofs on this page into an original arrangement called Abstricombo5:13 (Copyright © 2000 DarkBlues). He writes:

"Natural music has fascinated me for some time.... It is a strange music that seems to speak to the soul in a way that manufactured music cannot."

Copyright Considerations    All MIDI files linked to from this page are placed in the public domain (meaning they may be used for any purpose whatsoever, with or without acknowledgement, commercial or non-commercial, including use in a separate or derivative copyrighted work), with the following exception:

The "Abstricombo" arrangement is copyright © 2000 by DarkBlues.

The "78 RPM record label" image may be copyright and/or trademarked by says-it.com. The "Shape of Song" images are copyright by Martin Wattenberg. Any short attributed quotations may be copyright by their authors. All other text and images on this page are placed in the public domain.

See also Metamath Web Site - Copyright Terms.

This page was last updated on 3-Feb-2017. Your comments are welcome: Norman Megill metamath.org mirrors

W3C HTML validation [external]