[jnash]

Can't help but laugh at your comment. Mathematics is an informal social activity where humans try to convince other humans that certain abstract structures have certain properties. Having to turn those proofs into formal machine checked proofs makes a huge difference. Principia Mathematica was a big step forward and directly leading to Type Theory. It didn't succeed in what the authors tried to accomplish, but it very much had a massive impact on the world of mathematics. That's why we both know about it and discuss it today.