Oh neat. I recently spent a good bit of time comparing different formal proof systems. The Mizar project [0] is pretty interesting since it's proofs look a lot

Oh neat. I recently spent a good bit of time comparing different formal proof systems. The Mizar project [0] is pretty interesting since it's proofs look a lot like standard proofs in the literature. However, at the moment I'm a bit enamored with Metamath [1]. It's basically a tiny system that just performs formal substitution. Everything else, including propositional calculus, predicate logic, and ZFC set theory is encoded within the language, rather than the implementation. I.e. it's a metalogic that only knows about simple substitution. That way one can easily investigate other logics and axiom systems, e.g. they have stuff for intuitionist logics, orthomodular lattice models, you name it. Anyway, the project already has a pretty substantial collection of theorems, including a lot of analysis, topology, algebra and even QM. The cool thing is that you can easily dig up how the high level proofs trace back to the fundamental axioms, and there's no fancy math happening in the metalogic at all. Super cool stuff. [0]:http://www.mizar.org http://www.mizar.org [1]:http://metamath.org http://metamath.org