> If nobody understands a mathematical proof, does it count?
Nope. That's the social aspect of mathematics: your proofs have to be comprehensible and considered to be correct by those in the mathematical community that read them (at least peer review) before they're accepted.
A professor once defined a proof as "That which is convincing", and we were free to say, "I am not convinced"
While the topic being proven may be technically correct, the act of proving is a social act. The formal notation just makes this more precise than human language.
Proof is "that which is convincing to a fair and rational mind." It should compel a rational actor into the verifiable mitigation of some risk.
This particular fuss is one of the side effects of mathematicians' failing to properly adopt computers into their process. One of these days we will not accept a proof unless it is computer verified, and there will be no social aspect to it.
It should not matter if your proof is 10,000 pages if a computer can follow it.
It is still better to have a clean 1-page proof. There is no direct value for proving a theorem. Mathematics is nice because it's useful for further mathematics, useful for real-world applications, and beautiful. A 10,000 page proof that only a computer can follow is none of these things.
It is the second thing. Anyway, the number of pages is arbitrary -- it is a function of your language and terminology. Not every proof can be simplified, so surely there exist useful proofs that require 10,000 pages minimum for a given finite set of terms.
So you are very wrong. You are essentially asserting that the only mathematics worth doing is easy or already known in some compact form.
> surely there exist useful proofs that require 10,000 pages minimum
The classification of finite simple groups "consists of tens of thousands of pages in several hundred journal articles written by about 100 authors, published mostly between 1955 and 2004."[1]
That is a long proof, yes, but it doesn't support my point. One could easily imagine a formalization that could compress all that work into a single sentence. What you can't do is compress _all_ proofs to single-sentence proofs using a finite number of unique symbols.
We know that a computer can't verify all unknowable theorems. (Theory of Computation) But perhaps one can verify all provable theorems.
I suspect that computers will struggle on the cleverness factor, where proof requires joining multiple fields of math, rather than just running through algebraic manipulation.
Could a computer verify that the domino problem is undecidable? The proof consists of translating the problem into non-halting universal turing machines.
There's also a luck aspect. Perhaps Mochizuki's proof is comprehensible but no one has the desire to read it. A mathematician or scientist should be prepared to be a lone wolf, never receiving recognition and their groundbreaking ideas never known to another.
Nope. That's the social aspect of mathematics: your proofs have to be comprehensible and considered to be correct by those in the mathematical community that read them (at least peer review) before they're accepted.