Metamath Proof Explorer

Inspired by Whitehead and Russell's monumental Principia Mathematica, the Metamath Proof Explorer has over 6,000 completely worked out proofs in logic and set theory, interconnected with over a million hyperlinked cross-references. Each proof is pieced together with razor-sharp precision using a simple substitution rule that practically anyone can follow, not just mathematicians. Every step can be drilled down deeper and deeper into the labyrinth until axioms of set theory—the starting point for all of mathematics—will ultimately be found at the bottom. You could spend literally days exploring the astonishing tangle of logic leading, say, from 2+2=4 back to the axioms.