"What you get when you run mathematics through a disassembler." - Michael Schaeffer

I recently ran across a really cool website: metamath.org. Here's the site's description of itself:

Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. This site has a collection of web pages generated from those proofs and lets you see mathematics developed formally from first principles with absolute rigor. Hopefully it will amuse you, amaze you, and possibly enlighten you in its own special way.

The `symbol-pushing' part of mathematics has always appealed to me. I've often fantasized about deriving definitions from an absolutely minimal core and then creating an enormous database of theorems, all of which can be reduced to a sequence of typographic manipulations of axioms. That's exactly what this site does. The only fundamental symbols in the language of Metamath are the following:

• (arrow): implies
• (sideways backwards L): not
• (upside down A): for all
• (equals sign): equals
• (stylized epsilon): is an element of
• and (left and right parentheses)

All other symbols are simply shorthand notation for these. At the site, you can explore a database of thousands of theorems that result from various sets of axioms: propositional calculus, predicate calculus, and Zermelo-Fraenkel set theory with the axiom of choice.

What really makes Norman Megill (the creator) such a great guy is the fact that you can download the GPL'd source for the software used to build and verify the proofs in the Metamath language. Also available are a complete tarball of the entire site and a GFDL'd book about meta-mathematics and the Metamath software (with TeX source).

Seriously, folks, this site is one of the coolest things I've seen in a long time. If you enjoy formal systems, this site will make you very happy. On a random note, the website also has a page about converting the proofs to musical compositions.