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 that contribute to explaining why proofs can be incredibly difficult?
Best Answer
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:
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.