Maintained by MIT alumnus Norman Megill, Metamath is an ingenious language for expressing theorems in abstract mathematics, rigorously reducing them to a treelike network of proofs that can be verified by a computer program. Thus an expression like "2 + 2 = 4" can be traced back to its underlying axioms and shown to be valid through rigorous logic.

The proofs, of course, get quite a bit more complicated than that, spreading into propositional and predicate calculus and set theory. Strictly speaking, the site requires no knowledge of higher mathematics beyond the syntax of the proofs themselves; a lay user can verify the validity of each step even if she doesn't understand its "meaning," somewhat as a novice chessplayer can attest to the legality of a master game without understanding its significance.

Even so, the beauty of the rigor itself shines through as a great edifice of math rises on these granite foundations. New proofs are continually being added, and for the adventurous Megill has added facilities to explore Hilbert space and quantum logic and even a means to render mathematical proofs as music. Highly recommended.