The Truth Mines

In the Truth Mines, though, the tags weren't just references; they included complete statements of the particular definitions, axioms, or theorems the objects represented.

Every tunnel in the Mines was built from the steps of a watertight proof; every theorem, however deeply buried, could be traced back to every one of its assumptions. And to pin down exactly what was meant by 'proof', every field of mathematics used its own collection of formal systems: sets of axioms, definitions, and rules of deduction, along with the specialised vocabulary needed to state theorems and conjectures precisely.^*

I came across a cool maths site today (via Good Math, Bad Math). I'd actually been thinking about doing it myself for the last few years, but it always looked a bit too much like hard work (even when I had Copious Free Time), so I never quite got around to it.

It's kind of eerie, though—the proof pages are almost exactly like the ones I'd mocked up and had in my head when I was playing with the project (although less XML/MathML-y). I guess there aren't really that many different ways you could present it, but it does feel like some sort of noodly appendage has sucked the idea right out of my head and served it up as a completed web page (conveniently skipping the tedious business of doing all the work).

---

* Greg Egan, "Diaspora", 1997