If you cannot find proofs, talk about them.

Robert Reckhow with his advsior Stephen Cook famously started the formal study of the complexity of proofs with their 1979 paper. They were interested in the length of the shortest proofs of propositional statements. Georg Kreisel and others may have looked at proof length earlier, but one of the key insights of Reckhow and Cook is that low level propositional logic is important.

Today I thought we might look at the complexity of proofs.

Cook and Reckhow were motivated by issues like: How hard is it to prove that a graph has no clique of a certain size? Or how hard to prove that some program halts on all inputs of length ? All of these questions ask about the length of proofs in a precise sense. Proofs have been around forever, back to Euclid at least, but Cook and Reckhow were the first to formally study the lengths of proofs.

They were not directly interested in actual proofs. The kind you can find in the arXiv or in a math journal, or at a conference—online or not. The kind that are in their paper.

We are talking today about these types of proofs. Not proofs that graphs have cliques. But proofs that a no planar graph can have a clique.

Proofs

Proofs are what we strive to find ever day. They the coin that measures progress in a mathematical field like complexity theory. We do sometimes work out examples, sometimes do computations to confirm conjectures on small examples, sometimes consider analogies to other proofs. But mostly we want to understand proofs. We want to create new ones and understand others proofs.

Years ago when studying the graph isomorphism problem, I did some extensive computations for the random case. That is for the case of isomorphism for a random dense graphs against a worst case other graph. The computations helped me improve my result. It did not yield a proof, of course, but helped me realize that a certain lemma could be improved from a bound to . My results were dominated by paper of Laszlo Babai, Paul Erdös, and Stanley Selkow. Oh well.

Proofs Complexity

There are several measures of complexity for proofs. One is the length. Long proofs are difficult to find, difficult to write up, difficult to read, and difficult to check. Another less obvious measure is the logical structure of a proof. What does this mean?

Our idea is that a proof can be modeled by a formula from propositional logic. The is what we are trying to prove and the letters and so on are for statements we already know.

This is a direct proof. This is a proof by contradiction. This is proof that uses a statement that may be true or false.

The last is a slight cheat, we use to stand for a kind of axiom. A perfect example is from number theory. Let be the number of primes less than and the function the logarithmic function.

The prime number theorem says that

an error term.

It was noted that is larger than for known values. The obvious question was that could

be always true? If so this would be an interesting inequality. In 1914 John Littlewood famously proved that this was not true:

Theorem 1 If the Riemann Hypothesis is true:

is infinitely often positive and negative. If the Riemann Hypothesis is false:

is infinitely often positive and negative.

Thus he proved that

is infinitely often positive and negative whether the the Riemann is true or not.

Proofs in Trouble

A sign of a proof in danger is, in my opinion, is not just the length. A better measure I think is the logical flow of proof. I know of no actual proof that uses this structure:

Do you? Even if your proof is only a few lines or even pages, if the high level flow was the above tautology I would be worried.

Another example is . This of course is a circular proof. It seems hard to believe we would actually do this, but it has happen. The key is that no one says: I will assume the theorem to prove it. The flaw is disguised better than that.

I cannot formally define this measure. Perhaps it is known, but I do think that it would be an additional measure. For actual proofs, ones we use every day, perhaps it would be valuable. I know I have looked at an attempted proof of X and noticed the logical flow in this sense was too complex. So complex that it was wrong. The author of the potential proof was me.

Open Problems

Is this measure, the logical flow of a proof, of any interest?