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