[destring]

Can’t help but laugh at the phrase “Real formal mathematics”. Mathematics are as formal as required to be understood by the audience. After all, math is just a way to communicate abstract arguments and reasoning. Computers require more help to understand abstract concepts, doesn’t mean that formulation is better than our current one. See Principia Mathematica on why too much formalism is not a good idea.

[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.