Do you know about Metamath? “It 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 in complete detail from first principles, with absolute rigor. Hopefully it will amuse you, amaze you, and possibly enlighten you in its own special way.” Fascinating. You can even LISTEN to proofs http://us.metamath.org/mpegif/mmmusic.html!