Are there proofs in math which can't be verified by a single person in their life span (say $80$ years)?

Question

Are there any proofs in math that can't reasonably be verified in one human life span? Say $80$ years?

How about the four color theorem? Or Kepler conjecture?

Can a person theoretically prove any of these by hand in the course of their life time? Where we can assume they live for at least $80$ years? If these results can be proven by hand by one person in less than $80$ years, then does anyone know of other theorems which can't?

Obviously all this is rather vague and depends on the particular person etc. Also one could trivially create problems that require one to spend an enormous amount of time, for example verify that the $46576575476547665^{\text{th}}$ digit of $\pi$ in base $82$ is equal to $53$. So I'm asking in regards to more well known problems, not ones that were arbitrarily constructed like this souly to make it hard for someone to do by hand.

Again I'll iterate I know this is all still some what vague, but I'm interested in to what extent if any automated proof checking may become applicable in modern mathematics towards the near future. As I know for example automated proof checkers were used to verify the four color theorem and Kepler's conjecture, as no human was willing to go through and check them by hand (again I'm even not sure if its possible for a single human to verify either of these theorems all by hand).

Answer 1

I'll assume that various things such as "what a person can do in 80 years" and "what are allowed as proofs" are precisely defined and fixed.

With tongue in cheek, here is a way to get lots of such proofs. Since only finitely many proofs can be verified by someone within an 80 year period and there are infinitely many proofs, it follows that almost all proofs have the property that you're looking for.

Incidentally, I'd like to say that all you have to do is randomly choose a proof, because the probability will be $1$ that the proof you chose will be one of the proofs you are seeking. Unfortunately, there does not exist a uniform probability measure on a countably infinite sample space (the set of proofs).

Answer 2

In my opinion this very much depends on what is meant by verified.

Assuming that a proof is (loosely speaking) "a sound argument for the validity of a theorem", then I would interpret a verification of a supposed proof to be a way that I can convince myself (and others) that it is a sound argument. In this interpretation, a verification that takes more than a lifespan is not comprehensible for any human, so we can never know whether the supposed proof is an actual proof or just nonsense.

On the other hand, if we have computational tools, we can convince ourselves that certain arguments are sound by showing that the computational tool being used will generate a valid proof. Possibly we couldn't understand the proof as a whole, but if we know that each step is correct, then we can convince ourselves that the whole thing is correct as well. For example, if you want to prove that the sum $1+2+\dots+100000$ is equal to $5000050000$, you could of course evaluate the whole sum (and waste a large part of your life doing something utterly redundant). But it is very quick to prove that the sum of $1$ till $n$ always equals $\frac{n^2+n}{2}$ using natural induction, and just plug in the number.

In the same way that we believe natural induction, we can convince ourselves that an intricate proof is correct when it uses something like computer assistance. Without the need of understanding (or knowing) every step involved, we can understand how the proof is generated, and from that convince ourselves that every step is valid.

Finally, whether a proof is valid in the first place is also subject to interpretation. If you ask an intuitionist, then he would reject that the proof of the Intermediate Value Theorem is valid, as he believes proof by contradiction is fundamentally flawed. A finitist would reject that $\sum \frac{1}{2^n}=2$. Is it enough for you to believe that Fermat's Last Theorem is true (or if you do understand it, something equivalent in another field of mathematics that you haven't read), just because other mathematicians have checked the proof and didn't find a flaw, or are you only convinced after you have read and understood the proof yourself?

Answer 3

Shinichi Mochizuki's proof for abc conjecture.

In August 2012, Shinichi Mochizuki released a series of four preprints on Inter-universal Teichmuller Theory which is then applied to prove several famous conjectures in number theory, including Szpiro's conjecture, the hyperbolic Vojta's conjecture and the abc conjecture.Mochizuki calls the theory on which this proof is based "Inter-universal Teichmüller theory (IUT)". The theory is radically different from any standard theory and goes well outside the scope of arithmetic geometry. It was developed over two decades with the last four IUT papers occupying the space of over 500 pages and using many of his prior published papers.