Are there are any inherent mathematical reasons difficult proofs exist?

Question

This is not a complaint about my proofs course being difficult, or how I can learn to prove things better, as all other questions of this flavour on Google seem to be. I am asking in a purely technical sense (but still only with regards to mathematics; that's why I deemed this question most appropriate to this Stack Exchange).

To elaborate: it seems to me that if you have a few (mathematical) assumptions and there is a logical conclusion which can be made from those assumptions, that conclusion shouldn't be too hard to draw. It literally follows from the assumptions! However, this clearly isn't the case (for a lot of proofs, at least). The Poincaré Conjecture took just short of a century to prove. I haven't read the proof itself, but it being ~320 pages long doesn't really suggest easiness. And there are countless better examples of difficulty. In 1993, Wiles announced the final proof of Fermat's Last Theorem, which was originally stated by Fermat in 1637 and was "considered inaccessible to prove by contemporaneous mathematicians" (Wikipedia article on the proof).

So clearly, in many cases, mathematicians have to bend over backwards to prove certain logical conclusions. What is the reason for this? Is it humans' lack of intelligence? Lack of creativity? There is the field of automated theorem proving which I tried to seek some insight from, but it looks like the algorithms produced from this field are subpar when compared to humans, and even these algorithms are obscenely difficult to implement. So seemingly certain proofs are actually inherently difficult. So I plead again - why is this?

(EDIT) To rephrase my question: are there any inherent mathematical reasons for why difficult proofs exist?

Answer 1

Although this question may superficially look opinion-based, in actual fact there is an objective answer. The core reason is that the halting problem cannot be solved computably, and statements about halting behaviour get arbitrarily difficult to prove, and elementary arithmetic is sufficient to express notions that are at least as general as statements about halting behaviour.

Now the details. First understand the incompleteness theorem. Next, observe that any reasonable foundational system can reason about programs, via the use of Godel coding to express and reason about finite program execution. Notice that all this reasoning about programs can occur within a tiny fragment of PA (1st-order Peano Arithmetic) called PA⁻. Thus the incompleteness theorem imply that, no matter what your foundational system is (as long as it is reasonable), there would always be true arithmetical sentences that it cannot prove, and these sentences can be explicitly written down and are not that long.

Furthermore, the same reduction to the halting problem implies that you cannot even computably determine whether some arithmetical sentence is a theorem of your favourite foundational system S or not. This actually implies that there is no computable bound on the length of a shortest proof of a given theorem! To be precise, there is no computable function $f$ such that for every string $X$ we have that either $X$ is not a theorem of S or there is a proof of $X$ over S of length at most $f(X)$. This provides the (at first acquaintance surprising) answer to your question:

Logically forced conclusions from an explicitly described set of assumptions may take a big number of steps to deduce, so big that there is no computable bound on that number of steps! So, yes, proofs are actually inherently hard!

Things are even worse; if you believe that S does not prove any false arithmetic sentence (which you should otherwise why are you using S?), then we can explicitly construct an arithmetical sentence Q such that S proves Q but you must believe that no proof of Q over S has less than $2^{10000}$ symbols!

And in case you think that such phenomena may not occur in the mathematics that non-logicians come up with, consider the fact that the generalized Collatz problem is undecidable, and the fact that Hilbert's tenth problem was proposed with no idea that it would be computably unsolvable. Similarly, many other discrete combinatorial problems such as Wang tiling were eventually found to be computably unsolvable.

Answer 2

You received already good answers, but I want to add a point that has not been covered: combinatorics.

True, you may start with few simple assumptions and operations, but how many ordered ways are there to combine those assumptions? In a naive brute force approach, assuming that the shortest solution (ignore the fact that this is uncomputable, we just need a lower bound) takes n steps, including using assumptions or using operators; then there are $ n! $ ways to take all the n steps, but only 1 correct solution. And we do not even know n in advance!

So proofs are hard because naive brute force is not a working option.

Answer 3

Because all the easy proofs have already been proven or are trivially easy.

I can write down an infinite series of assertions that have never been proven:

(A) Prove that $465458891113223521658103238 + 1 = 465458891113223521658103239$

(B) Prove that $465458891113223521658103239 + 1 = 465458891113223521658103240$

(C) Prove that $465458891113223521658103240 + 1 = 465458891113223521658103241$

None of these problems have ever been stated, much less proven, before. (Seriously -- Google any of those numbers! They've never been written down before.) However, they are each trivially easy to prove: indeed it's quite enough to say that they immediately follow from the definitions of how numbers work and what $+$ does.

So it's clear that there are infinitely many "easy" proofs. Why don't we see more easy proofs being discussed in math journals? Because they're boring, and we don't learn anything new from them.

So the question is not really "why are proofs difficult", but rather "why are the proofs that anyone ever talks about difficult?" and the answer is: well, the entire reason they're interesting is because they're difficult. Mathematicians spend a ton of time exploring the space of possible proofs to find exactly those ones that are difficult and interesting. Proofs are written specifically to cover as much "ground" as possible, so that once they are proven, there are no "trivially similar" proofs that remain unproven (in the way that A, B, and C above are all trivially similar). So there's simply nothing left to prove that is both easy (with our current proof techniques) and interesting.

Of course, every once in a while a proof that seemed extremely hard turns out to actually be easy. These are the most interesting proofs of all, because they tend to teach us a lot about our proof techniques.

Answer 4

The difficulty comes from abstraction. Mathematics is a layered subject. Each topic is built on a complex foundation of many slightly simpler topics, which are in themselves all abstractions of more fundamental ideas. You may as well ask why some computer programs are so complicated. For the most part, any one of thousands of lines in a complex computer program is not that complex. But, when multiple different processes are abstracted and put together, understanding how the program works, and debugging it, becomes very difficult.

Sometimes the difficulty in proofs comes from the fact that you have to start with a whole onion, peel it layer by layer until you get to the core, and then rebuild it from the ground up.

Answer 5

I will try to complement the discussion. I think the question is also linked to this other: why is so hard to choose good axioms?

Of course every theorem, even Poincaré Conjecture, is trivial if we insert it as an axiom in a system (we can always do that for a true formula). We could be less extreme and reduce to axioms only the difficult lemmas used to proof something. Then the theorem would follow easily. Take for example the classical triad of equivalent theorems in set theory: the Well-ordering Theorem that states that every set can be ordered; the Zorn lemma and the axiom of choice. There is a joke that says:

The axiom of choice is obviously true, the well-ordering principle obviously false, and who can tell about Zorn's lemma?

It is complex (at least for me) to proof the Zorn lemma from the axiom of choice. But the well-ordering principle follows easily from the Zorn lemma. See the discussion on the above link.

Reverse mathematics is the fields that do the following: give me theorems and I will find which axiom is needed. What seems interesting to me is that this approach allows someone more philosophically inclined to be more precise about things he want to avoid.

But let say our philosophy is something like a proof pragmatism: given a set of theorems, is there a optimal axiom system for it? With optimal we mean not only the size of axiom, but perhaps also time of computation consumed (or both of them). Well, if we can assume that the set of axiom and the set of rules operating it can be implemented in a computer, this question turn to be linked to computational complexity. In special, there is an analogous of the Gödel Incompleteness theorem in this context, called Chaitin Theorem.

There is also one thing worth mentioning I think: given the truth value of some propositions, to verify if some formula of proposition logic is true is a piece of cake, just substitute the truth values in it. Given a formula, to find the truth values that turn the formula true: that is more difficult, in some cases the computers we have today can do it, and in the worst case will take a lot of time (not viable for our computers). This is the SAT-problem. But this problem will be still decidable by any abstract computer (a computer that don't have problems of time): do the truth table. Now the problem seems to start when we have a logic with predicates and quantifiers. It is not decidable by any abstract computer to know whether a formula in predicate logic is satisfatible.