Alfred North Whitehead and Betrand Russell wrote Principia Mathematica, which apparently effectively reduced much of Mathematics to Set Theory, as Metamath seems to do.
Of course, it is said that W. V. Quine was the last living person to have actually read the Principia; perhaps the interactivity added by Metamath will make the latter project more successful?
Slashdot Mirror
Of course, it is said that W. V. Quine was the last living person to have actually read the Principia; perhaps the interactivity added by Metamath will make the latter project more successful?