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.

  • 5
    $\begingroup$ It shouldn't be possible due to Goedel's Incompleteness Theorem. $\endgroup$ – Ron Gordon Dec 28 '12 at 15:06
  • 1
    $\begingroup$ 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. $\endgroup$ – Thomas Andrews Dec 28 '12 at 15:07
  • $\begingroup$ 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! $\endgroup$ – Peter Smith Dec 28 '12 at 15:17
  • 1
    $\begingroup$ 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. $\endgroup$ – Thomas Andrews Dec 28 '12 at 15:23
  • 2
    $\begingroup$ 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? $\endgroup$ – 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.

  • $\begingroup$ nit. technically true but I think the spirit of the question is "can all provable theorems in mathematics be expressed in Coq?" $\endgroup$ – Frank Bryce Jan 16 at 1:54

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?


Coming from a practical angle (i.e., not discussing the limits on logic that we know about due to the incompleteness theorem etc), your question might be rephrased as "Can we do all of the math that we do on paper, in Coq?"

The answer is "Dunno, it's tough. We'll get back to you." You're not the first person to think so though, and there are efforts to "put math on computers". Check out Homotopy TT.

To elaborate a bit: The main reason is that a large portion of mathematics is done using set theory as the working foundation, but set theory is not amenable to being expressed with computers. It's too declarative. The internal logic in Coq (Calculus of Co-inductive Constructions) is based on Martin-Löf Type Theory, which is a quite a different kettle of fish. So some definitions, although equivalent, aren't the same, and some of the low level stuff is not built up in the same way.

Widening the gap between the paper and machine worlds is that there is a preference for Constructive Math in the machine world. (oversimplifying: a preference for not using the law of excluded middle (or equivalent classical axioms/rules)) and intuitionistic logic.

Addendum: What I've been talking about above is how the logical foundations of coq are different from traditional foundations. That said, Coq is still doing math, that requires logical foundation, that is still subject to the limitations of formal logic. The incompleteness theorems etc.

P.S. - No physical computer system can by guaranteed bug free by mathematics. Even if your hard and software is verified, cosmic radiation/favourite energy source may cause bits in your machine to flip and all your verification goes out the window. Even with verification, some programs should be run in triplicate.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.