Als Metamath siehe http://us.metamath.org/

I've only taken a quick look at this yet, but that was enough to tell me to post this link here: http://us.metamath.org/ Front page excerpt: Metamath Proof Explorer - Constructs mathematics from scratch, starting from ZFC set theory axioms. Over 6,000 proofs. Hilbert Space Explorer - Extends ZFC set theory into Hilbert space, which is the foundation for quantum mechanics. Includes over 1,000 complete formal proofs. Quantum Logic Explorer - Starts from the orthomodular lattice properties proved in the Hilbert Space Explorer and takes you into quantum logic with around 1,000 proofs. Metamath Solitaire - A Java applet that demonstrates simple proofs. Built-in axiom systems include ZFC; modal, intuitionistic, and quantum logics; and Tarski's plane geometry. GIF and PNG Images for Math Symbols - A copyright-free collection of over 1,000 bit-mapped images for math symbols. Metamath Music Page - Strictly for fun. You can listen to what mathematical proofs "sound" like! 21-Jan-2006 Some advanced and difficult miscellaneous open problems related to Metamath and other topics on this site. Mini FAQ Q: What is Metamath? A: 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 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. Q: Will Metamath help me learn abstract mathematics? A: In order to follow a proof in an advanced math textbook, you may need to know prerequisites that could take years to learn. This frustrates a lot of people. In contrast, Metamath uses a single, simple substitution rule that allows you to follow any proof mechanically. You can actually jump in anywhere and be convinced that the symbol string you see in a proof step is a consequence of the symbol strings in the earlier steps that it references, even if you don't understand what the symbols mean. But this is quite different from understanding the meaning of the math that results.