# Is it possible to prove everything in mathematics by theorem provers such as Coq?

Coq has been used to provide formal proofs to the Four Colour theorem, the Feit–Thompson theorem, and I'm sure many more. I was wondering - is there anything that can't be proved in theorem provers such as Coq?

A little extra question is if everything can be proved, will the future of mathematics consistent of a massive database of these proofs that everyone else will build on top of? To my naive mind, this feels like a much more rigorous way to express mathematics.

-
It shouldn't be possible due to Goedel's Incompleteness Theorem. –  Ron Gordon Dec 28 '12 at 15:06
Define "everything" and "possible" :) It's not clear from what I've read that Coq "proved" Feit Thompson, only that it verified a proof. In theory, you can write a "dumb" proof generator that checks all possible proofs for correctness, and thus yields all provable results. Coq might be more efficient, but it cannot be more complete than that. –  Thomas Andrews Dec 28 '12 at 15:07
Putting it briskly, Gödel's First Incompleteness Theorem uses rather elementary reasoning (and it was very important to Gödel that this was the case). Which is why the Theorem is formalizable in arithmetic, the point we rely on to prove the Second Theorem! –  Peter Smith Dec 28 '12 at 15:17
Sure, but there is an "internal" meaning to incompleteness, and an "external" meaning to incompleteness. Basically, it is just saying that sufficiently complicated axioms cannot yield complete systems. That some axiom systems are incomplete is obvious (take the axiom for a ring and try to resolve the question "Is 1+1=0?") The shock of incompleteness is that we want our axioms to represent something, the natural numbers, we feel is "concrete." Essentially, complicated systems of axioms will have to be like the axiom for a ring. –  Thomas Andrews Dec 28 '12 at 15:23
The set of theorems of a computably-axiomatised first-order theory is computably enumerable – this is indisputable. So perhaps the question should be, can all of mathematics be captured in a sufficiently powerful first-order system? –  Zhen Lin Dec 28 '12 at 15:28

One of the computability results is that there must exist provable theorems in number theory that require very long proofs relative to their statements.

If $n$ is the encoding of a statement in number theory which can be proven, and $f(n)$ is the length of the shortest proof of that statement, then the function $$G(n)=\max \{f(k): k\leq n, k \text{ encodes a provable theorem}\}$$ is not only not computable, but it cannot be bounded above by any computable function, or else we could write a program that could essentially "find" all decidable statements - the set of decidable theorems would be recusrive, not just recursively enumerable. (I initially had an argument here about why that would be a problem, but that argument was flawed. I'm still pretty sure it is wrong for the decidables to be recursive, but it will take more work.)

In particular, then, for any total computable function $h$, there must be a provable theorem encoded by some $n$ such that the shortest proof, when encoded, is greater than $h(n)$.

So, in a practical sense, there will always be harder theorems, where we need more storage and compute time to verify the entire proof.

-

It is reasonable to believe that everything that has been (or can be) formally proved can bew proved in such an explicitly formal way that a "stupid" proof verification system can give its thumbs up. In fact, while typical everyday proofs may have some informal handwaving parts in them, these should always be able to be formalized in a so "obvious" manner that one does not bother, in fact that one is totally convinced that formalizing is in principle possible; otherwise one won't call it a proof at all. In fact, I sometimes have the habit to guide people (e.g. if they keep objecting to Cantor's diagonal argument) to the corresponding page at the Proof Explorer and ask them to point out which particular step they object to.

For some theorems and proofs this approach may help you get rid of any doubts casting a shadow on the proof: Isn't there possibly some sub-sub-case on page 523 that was left out? But then again: Have you checked the validity of the code of your theorem verifier? Is even the hardware bug-free? (Remember the Pentium bug?) Would you believe a proof that $10000\cdot10000=100000000$ that consists of putting millions of pebbles into $10000$ rows and columns and counting them more than computing the same result by a long multiplication?

-

It is unlikely that Archimedes thought about theorems in category theory. In the future there will likely be new areas of mathematics. While a theorem prover might have encodings of results in these new areas they might not be readable for humans.

-