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?

  • 11
    $\begingroup$ There are proofs at every level of difficulty. You hear mostly about the most difficult ones because they’re, well, the most difficult. $\endgroup$
    – Deane
    Apr 28 at 13:13
  • 12
    $\begingroup$ This is very vague. You could just as easily ask the opposite question: "why is it that so many interesting results have proofs that can be written out at lengths understandable by people?" A priori, maybe interesting things sholud be undecidable, or maybe they should have proofs that would take a billion pages. Maybe these things tell us something about the nature of mathematics, maybe they tell us something about the sort of problems we are willing to call "interesting". $\endgroup$
    – lulu
    Apr 28 at 13:18
  • 6
    $\begingroup$ To perhaps give a somewhat heuristic answer: if at any point in some logical derivation there are a finite number of possible "things I can do", say, $b$, then after $n$ "steps" in the proof, there are a total of $b^n$ possible "states" the proof could be in. Exponentials grow quickly, and there is no a priori bound on how big $n$ could be. $\endgroup$ Apr 28 at 13:28
  • 23
    $\begingroup$ "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!" ... This reminds me of the Michelangelo quote: "Sculpting David is easy: Just take a big block of marble and chip away everything that isn't him." (Actually, Michelangelo might never have said that; at least, not in exactly that way. See Quote Investigator.) $\endgroup$
    – Blue
    Apr 28 at 13:40
  • 9
    $\begingroup$ Why is life so difficult in general? $\endgroup$ Apr 28 at 14:27

5 Answers 5


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.

  • $\begingroup$ And, by the way, the situation is still very bad even for decidable theories with quantifier elimination such as Presburger arithmetic, for which theorems of length $n$ have worst-case proof length of $2^{2^{Ω(n)}}$ (doubly-exponential). For another example, RCF is a useful decidable theory for which it seems the best known algorithm for finding a proof or disproof of a statement of length n takes $2^{2^{O(n)}}$ time. $\endgroup$
    – user21820
    Apr 28 at 14:41
  • 1
    $\begingroup$ Thank you for the technical answer - exactly what I was looking for. However, I am only slightly familiar with many of the concepts you reference here, but really want to make sense of your answer. Could explain in slightly more unfamiliar terms? Or point me to resources explaining these concepts? $\endgroup$
    – A. Lavie
    Apr 28 at 17:29
  • $\begingroup$ @A.Lavie: Well, the first thing you need to do is to learn basic programming, and then understand the halting problem and why it is computably unsolvable (i.e. there is no program H such that for every program P and input X we have that H(P,X) halts and outputs 1 iff P halts on X). After that, the key point is that statements of the form "P halts on X" can be expressed as arithmetical sentences (i.e. that quantify only over ℕ), and it is also very easy to write down arithmetical conjectures such as "∀k∈ℕ ∃p∈ℕ ( p > k and Prime(p) and Prime(p+2) )". [cont] $\endgroup$
    – user21820
    Apr 28 at 17:41
  • 3
    $\begingroup$ There is a very decent argument to be made that it's less about the Halting problem and more about P vs. NP. I will try to write down an answer about it unless someone beats me to it. The halting problem is more about things being undecidable and unprovable, but doesn't really answer why it is that it's hard to find proofs of short and provable assertions. $\endgroup$
    – DRF
    Apr 28 at 21:54
  • 3
    $\begingroup$ @DRF: No, did you not read what I emphasized in bold, which is that there is no computable bound on proof length even if you are assured that it is provable? This goes way beyond the phenomenon of easy verifiability of a solution to an NP problem! If the question was about finding short (i.e. polynomial-length) proofs when a short proof is guaranteed to exist, then it would be related to NP, but that was not the question, and it is definitely is not the key phenomenon faced by a mathematician tackling a general number theoretic conjecture. $\endgroup$
    – user21820
    Apr 28 at 22:04

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.


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.

  • 2
    $\begingroup$ I think my question was slight misunderstood. In the context of your thinking, my question becomes: why aren't all proofs easy? Why are some propositions inherently hard to prove? That's different from: why are all interesting proofs hard? $\endgroup$
    – A. Lavie
    Apr 28 at 23:27
  • 1
    $\begingroup$ @A.Lavie It'd be incredibly surprising if no proofs were difficult. Given that any proofs are difficult, my above answer holds. But see user21820's excellent answer as to why proofs can be arbitrarily hard. Basically, we can just write arbitrarily complex statements to prove. "Prove that X Turing Machine Halts". $\endgroup$ Apr 28 at 23:34
  • $\begingroup$ I don’t think you can prove that a number that gets no hits in a google search has never been written down before. It’s trivial to prove that the internet does not contain everything that’s ever been written down. $\endgroup$ Apr 29 at 4:15
  • $\begingroup$ @ToddWilcox I was being a bit glib there, to illustrate how easy it is to come up with a new "proof" that nobody has ever proven before (and to show there are infinitely many of these). If a random-ish 27-digit number is not enough for you to be confident it's a never-before-written number, just make it 100 digits, or 1000. $\endgroup$ Apr 29 at 6:04

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.


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.

  • 1
    $\begingroup$ That's right! Indeed, if we stay within PL (propositional logic) then the hardest kind of problems we can face is essentially NP-complete problems. But moving from PL to full FOL pushes the difficulty all the way into undecidability, and there is no nice gap in-between; reverse mathematics shows us that even just arithmetical sentences can fall across a vast yet very fine spectrum of difficulty to prove. Regarding Zorn's lemma, you may be interested in this short proof. $\endgroup$
    – user21820
    Apr 29 at 6:50
  • 1
    $\begingroup$ @user21820, wow that was a nice short proof of Zorn's lemma! Thank you for sharing. $\endgroup$ Apr 29 at 14:45
  • $\begingroup$ You're welcome! Essentially the same technique yields a 1-line proof of the well-ordering theorem. $\endgroup$
    – user21820
    Apr 29 at 15:17

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.