Verifying proofs is a much simpler job than creating a proof. Also, you can have multiple independently implemented verifiers, which act in many ways like multiple human reviewers. That is what the metamath community does, they have 4 independently implemented verifiers that check every proof. That is very strong evidence that a proof is correct, far stronger evidence than is typically accepted now.
Yes but these will only accept proofs from within the mathematical framework of the multiple verifiers. I'm not saying that having 4 automatic independent verifications of a proof is useless, far from it! Just that, the notion you can "prove" all of mathematics is almost meaningless, or demonstrable false.
I'm not sure what your point is here. If the point is that the provers require a particular format, and not just English sentences, then that is true but not really a problem. Writing programs also requires that you use a particular format, AKA programming language, and that happens all the time.
It's true that some things cannot be proven, due to Goedel's incompleteness theorems... but that is a fundamental limitation of mathematics and has nothing to do with the limitations of computer tools.
You can write proof verifiers that are very generic. The metamath proof verifiers, for example, can work with arbitrary axiom systems. Most people use metamath to prove statements using classical logic with ZFC, but there are a number of other systems that are supported. Quine's New Foundationd set theory axioms and intuitionistic logic are alsk supported.
"I don't really understand why the entire known mathematics is not automatically proven yet."
Which I believe is going to be related to English (or whatever natural language) if we really want to talk about what is meant by "entire known mathematics".
edit: I mean it's a crazy proposal, so you get a crazy response. I think somewhat intuitively we know you can't prove everything.
