Hey - thanks for actually replying and taking me seriously. This is as far as this discussion has ever gotten between me and someone who seems to know what they are doing. I'm actually learning a lot.

> It's because we have essentially picked the parts of mathematics we're going to force to be true about half way up the stack. If the axioms don't permit those theories, then we'll do away with the axioms and pick a different set.

Is this related to the famous incompleteness theory? If you hit a proof that you can't prove with this set of axioms, you just try another one? It blows my mind that you can just pick any set of axioms you like. It feels like there should be a set of core axioms that is the fundamental truth. Maybe it's time that I read G.E.B and the Principia. Any recommendations for these kinds of questions?

> So you question about why libraries don't exist is essentially "Why have mathematicians not replicated hundreds or thousands of years of effort in to a format that's hard for them to personally use, but is good for these tools we've developed in the past couple decades?"

Okay, so people are working on it. It seems like a miracle that the alternative of "we're doing it all in our heads" actually works:

> Mathematicians generally don't evaluate the truth of a new paper relative to the axioms, but relative to the already established results in a field.

This is what I'm taking about. What if - somewhere in the middle - there was a mistake?

...

> Why do you think mathematics should be more standardized than programming? (Actually, I'd argue it's already more standardized than programming, and you're arguing for some kind of extreme position.)

My main concern is - every year we get someone who thought they proved, for example, P != NP, only to find a few months and a billion man hours later that there is a minute error on page thirty-five where the author misunderstood and overlooked some very subtle thing. Wouldn't it me much more pleasant if this task was automated?

Wouldn't it be amazing if we could use machine learning methods or tree search methods to formulate a proof mechanically? Or automatically eliminate proof steps to make them less complicated! Compiler-style optimization if you will. Wouldn't it be amazing if thousands of existing proofs could be analyzed statistically? Wouldn't it be great if we could machine-translate standardized proofs into regular ol' mathematical notation or whatever language we want? When we have the ability in the future, we can go back and verify them all en masse! Am I deluded in thinking any of this could be valuable?

> You seem to imply that mathematical notation should be standardized, but are omitting that even languages explicitly meant for computation are not.

Well, at least programming languages without standards have an implementation that is the official implementation! So arguably, they are more standardized.

Anyway, thanks for replying, I haven't had such an interesting exchange on HN in a while. I'm eagerly awaiting your response (if you have the time)!

edit: Also it seems like learning a standardized mathematical notation would be only marginally harder that learning to typeset regular mathematical notation in latex! Heck, you could have it compile down to latex.

edit2: Another thought I had was, since mathematicians don't prove things all the way from the bottom axioms up, but from the closest accepted truth, couldn't we have verification systems do that instead? That seems a more easily reachable goal.