http://us.metamath.org/mpegif/mmmusic.html
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)
There was a time when you'd learn music along arithmetic, geometry and astronomy, because they all deal with Harmony. Boethius named this cursus the quadrivium.
In liberal arts education, the quadrivium consists of the four subjects or arts (namely arithmetic, geometry, music, and astronomy), taught after teaching the trivium. The word is Latin, meaning four ways, and its use for the four subjects has been attributed to Boethius or Cassiodorus in the 6th century. Together, the trivium and the quadrivium comprised the seven liberal arts (based on thinking skills), as distinguished from the practical arts (such as medicine and architecture).
For most medieval scholars, who believed that God created the universe according to geometric and harmonic principles, science – particularly geometry and astronomy – was linked directly to the divine. To seek these principles, therefore, would be to seek God.
The quadrivium consisted of arithmetic, geometry, music, and astronomy. These followed the preparatory work of the trivium, consisting of grammar, logic, and rhetoric. In turn, the quadrivium was considered the foundation for the study of philosophy (sometimes called the "liberal art par excellence") and theology. The quadrivium was the upper division of the medieval education in the liberal arts, which comprised arithmetic (number), geometry (number in space), music (number in time), and astronomy (number in space and time) Educationally, the trivium and the quadrivium imparted to the student the seven liberal arts (essential thinking skills) of classical antiquity.
The author of the metamath's webpage uses a program to visualize music structure. For instance, here's the visualization of the structure of the tune of the Schröder-Bernstein Theorem: http://us.metamath.org/mpegif/_music_shape_mm.gif
Now compare the last image to an actual illustration found in Boethius' book de Institution Musica: http://www.chmtl.indiana.edu/tml/6th-8th/BOEMUS2C_05GF.gif
How quaint!
