HomeMetamath Home 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

    New 29-May-2006  A digg.com discussion [external] about this page.


    Mathematical Proofs Set to Music    I added this web page just for fun. While looking at some proofs, it Triangle Inequality played on black keys only 1:49 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 [external].

    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 MIDI file0:16. Other times the effect is significant; compare the syncopatedMIDI file1:49 and non-syncopatedMIDI file1:49 versions of the Triangle Inequality (and also another version). Another curious piece with a pronounced syncopated effect is the Square Root Theorem MIDI file0: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 MIDI file3: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 MIDI file0:50. The Schröder-Bernstein Theorem MIDI file1: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 MIDI file0:05
  • Peirce's axiom MIDI file0:03
  • Praeclarum theorema MIDI file0:06
  • Proposition *5.18 from Principia Mathematica MIDI file0:47
  • Existential quantifier introduction MIDI file0:10
  • x = x MIDI file0:10
  • Existential elimination by uniqueness MIDI file0:03
  • Basic relationship between class and wff variables MIDI file0:10
  • Two ways of saying "is a set" MIDI file0:06
  • Derivation of Separation Axiom MIDI file0:41
  • Derivation of Empty Set Axiom MIDI file0:02
  • Derivation of Pairing Axiom MIDI file1:30
  • Subset defined in terms of set difference MIDI file0:32
  • Russell's paradox MIDI file0:20
  • Associativity of function composition MIDI file1:41
  • Function value in terms of ordered pair MIDI file0:06
  • Cantor's theorem MIDI file1:27
  • Mathematical induction MIDI file0:14
  • Peano's postulates: 1 MIDI file0:06 2 MIDI file0:16 3 MIDI file0:01 4 MIDI file0:35 5 MIDI file3:39
  • The existence of omega MIDI file0:20
  • Transfinite induction MIDI file1:19
  • Transfinite recursion MIDI file0:18
  • Schröder-Bernstein Theorem MIDI file1:47
  • Pigeonhole Principle MIDI file2:35
  • Axiom of Choice equivalent MIDI file3:51
  • Zermelo's well-ordering theorem MIDI file0:50
  • Zorn's Lemma MIDI file5:05
  • The 27 postulates for real and complex numbers: 1 MIDI file0:01 2 MIDI file0:06 3 MIDI file0:02 4 MIDI file0:06 5 MIDI file0:51 6 MIDI file0:27 7 MIDI file1:34 8 MIDI file0:27 9 MIDI file0:09 10 MIDI file0:34 11 MIDI file0:39 12 MIDI file6:46 13 MIDI file3:37 14 MIDI file0:06 15 MIDI file0:34 16 MIDI file1:13 17 MIDI file2:16 18 MIDI file7:45 19 MIDI file1:20 20 MIDI file1:45 21 MIDI file1:14 22 MIDI file0:04 23 MIDI file0:04 24 MIDI file1:59 25 MIDI file1:17 26 MIDI file3:11 27 MIDI file4:37
  • Archimedean property of real numbers MIDI file0:58
  • Square root theorem MIDI file0:41
  • Complex number in terms of real and imaginary parts MIDI file0:02
  • Complex conjugate MIDI file0:12
  • Triangle inequality for absolute value MIDI file1:49
  • 2 + 2 = 4 for complex numbers MIDI file0: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 [external] Java applet. At the top we show the Schröder-Bernstein Theorem MIDI file1: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-02:  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 5,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 [external].

    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 MIDI file1: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:

    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.

    For Unix/Linux/MacOSX:
    Obtain the t2mf program from http://www.hitsquad.com/smm/programs/mf2t/download.shtml [external]. Follow the instructions for compiling it and put it into a binaries directory.

    Note added 30-Dec-2003: The source files were apparently removed from the above download, and only the Windows binaries remain. I located a copy of the source files at ftp://ftp.cs.ruu.nl/pub/MIDI/PROGRAMS/mf2tsrc.zip [external] but it is unclear if they will compile on modern C compilers. If someone is successful at doing this, let me know and I will put the instructions here. Otherwise, you may have to borrow a Windows machine to run t2mf.exe.
    Update added 9-May-2006: Luca Ciciriello has upgraded the t2mf program, which is a C program used to create the MIDI files on the Metamath Music Page, so that it works on MacOS X. This is a nice accomplishment, since the original program was written before C was standardized by ANSI and will not compile on modern compilers.
          Unfortunately, the original program source has no copyright terms. The main author, Tim Thompson, has kindly agreed to release his code to public domain, but two other authors have also contributed to the code, and so far I have been unable to contact them for copyright clearance. Therefore I cannot offer the MacOS X version for public download on this site until this is resolved. Update 10-May-2006: Another author, M. Czeiszperger, has released his contribution to public domain.
          If you are interested in Luca's modified source code, please contact me directly until the copyright issues are resolved.

    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
    


    The Algorithm    I'll use as an example the simple theorem id1 which is the Law of Identity MIDI file0: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 id1 / normal
    
    Then we type
      MM> show proof id1 / 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 id1 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 id1 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 MIDI file0: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 MIDI file1: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 has combined a few of the proofs on this page into an original arrangement called AbstricomboMIDI file5: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 29-May-2006.
    Your comments are welcome: Norman Megill nm at alum dot mit dot edu
    metamath.org mirrors
    W3C HTML validation [external]