Suppose we have an axiom system and theorems derived out of that axiom system, is there any way to rigorously speak about a theorem being more difficult to prove than others?

In my personal thoughts, I think maybe we can take the difficulty to prove the theorem as in the number of steps in the shortest proof of it... but a disadvantage of this way is that it maybe that a longer proof is actually a psychologically easier to understand.

Are there other ways?


Suppose in the future that for some reason that we derive a contradiction from the existing foundation of mathematics then I was contemplating how one could try to salvage it into something which is still contradiction free.

A thought which come in this contemplation was, Would the theorems of lesser difficulty, for a suitable definition of difficulty, be more possible to retains than others in the salvaged axiom system?

Example: I am thinking of a situation like the day when Russel Paradox was discovered. If I have understood it correctly, the issue was stemmed out of how the axiom of comprehension was written.

The interesting thing was that even when ZFC came, we were able to implement many of the conceptual ideas we had in Set theory in the Naive set theory back in it. So, the thought was, could there be a way to quantify the difficulty so that we could say think things like "hmm these theorems would could survive even if the foundations were a bit different".

Tangentially related question on Philosophy.SE and Reverse Mathematics: figuring out what axioms a theorem is equivalent too

  • 2
    $\begingroup$ For your same statement in the second paragraph. The question needs to be better stated, what does it mean to you that one proof is more difficult than another? There are some proofs about the infinity of prime numbers, are the topological proofs more difficult than the arithmetic ones? why? You need to better define the term you use to refer to "difficult." $\endgroup$
    – A. P.
    Jul 20, 2022 at 11:10
  • $\begingroup$ I mean it's a conceptual thing which could possibly define in many different ways. Getting into philosophy here, but imo, usually any attempt at pinning down a conceptual idea through a definition comes with some information loss. I am looking for possible ways to do this rather than an exact answer. @user1027216 $\endgroup$ Jul 20, 2022 at 11:13
  • $\begingroup$ Look into proof theory: en.wikipedia.org/wiki/…. Maybe model theory also. I know nothing about them... $\endgroup$ Jul 20, 2022 at 11:15
  • $\begingroup$ What do you mean, "we can derive a contradiction from the existing foundation of mathematics " ? You're talking about inconsistency/ incompleteness (Godel incompleteness-related) stuff? $\endgroup$ Jul 20, 2022 at 11:20
  • 1
    $\begingroup$ Here's how you measure how hard a theorem is: you take the number of years it was an open problem, and multiply by the number of mathematicians who worked on it. You might want to weight each mathematician by how much time he/she spent working on the problem, and/or by how good a mathematician he/she was (though of course that raises the question of how you decide how good a mathematician is). Some of this data may be difficult to come by. $\endgroup$ May 2 at 3:42

1 Answer 1


There are several ways you can quantify how difficult a theorem is, each having its own advantages and disadvantages.

Proof complexity

In your question, you suggested looking at the number of "steps" it takes to prove a theorem as a measure of the difficulty of proving that theorem. However, the number of steps it takes to prove a given theorem depends on which proof system you are using to formalize your proofs. In fact, the field of proof complexity is more commonly used to compare entire proof systems to each other, and not to compare specific theorems to each other. For example, an open problem in proof complexity is to determine whether or not there exists a "polynomially bounded" proof system (i.e., a proof system that can prove all propositional tautologies via proofs whose sizes are polynomial in the sizes of the tautologies).

So, it might not be sensible to speak of "the" proof complexity of a given theorem, because it depends on which formal system you are using. Additionally, like you said, the size of a proof might not reflect how difficult the proof is for a human brain to come up with.

Reverse mathematical strength

The program of reverse mathematics aims to determine which axioms are necessary to prove which theorems. It works like this:

  1. Start with a "base theory", which is not strong enough to prove most of the theorems you are interested in. A base theory should be a strict subset of the axioms that are generally accepted by mathematicians. One common base theory used is $\text{RCA}_0$.

  2. Select a theorem that you would like to analyze.

  3. See which other axioms you are able to prove assuming this theorem (over the base theory).

  4. See if you can prove the selected theorem assuming these other axioms (over the base theory).

If you are successful, you will have proven that a given theorem is equivalent to some certain axioms (over the base theory). Here's an example: over $\text{RCA}_0$, the Heine-Borel Theorem is equivalent to the axiom Weak König's Lemma, but the Bolzano-Weierstrass Theorem is equivalent to the Arithmetical Comprehension Axiom. It happens that the Arithmetical Comprehension Axiom implies Weak König's Lemma but that the converse is not true. So, we can say that the Bolzano-Weierstrass Theorem is "stronger" than the Heine-Borel Theorem, since it requires axioms that are strictly more powerful.

So, reverse mathematical strength is a measure of how "high-powered" the machinery needed to prove a theorem is. However, like proof complexity, it doesn't say anything about how hard a proof of it is for a human brain come up with.

Subjective analysis

Ultimately, if you want to talk about how difficult a theorem is for humans to prove, you will need some kind of subjective measure, since the difficulty of a theorem depends on how we think, what kind of strategies and techniques we are taught in school, what mathematical facts we happen to know, etc.

One subjective scale for analyzing the difficulty of proofs is the Math Olympiad Hardness Scale (MOHS) created by Evan Chen. However, this scale is specifically for Math Olympiad problems, and not for theorems in general. Additionally, it is based on precedent (what types of problems have been included on the International Mathematical Olympiad in the past), so it could change over time.

If you want to assess how difficult theorems in general are, you could consider where they appear in standardized curricula and assume that the designers of these curricula organized them by difficulty.

Additionally, you might want to take a look a John Conway and Joseph Shipman's paper Extreme Proofs I: The Irrationality of $\sqrt{2}$. In this paper, they consider different proofs of the fact that the square root of $2$ is irrational, and they explain why they are "extreme" in various senses. For example, one proof is the "most general," another depends on the "simplest concepts," and another is "purely geometrical."

Regarding your dream for salvaging inconsistency

The project of reverse mathematics has done much to classify foundational theories based on how strong they are. If one of these foundational theories is proven to be inconsistent, we could certainly "fall back" on a strictly weaker theory, and the program of reverse mathematics would tell us which theorems we would "lose" by abandoning our strong system.

Most mathematicians are extremely confident that all of the theories we use are consistent. However, we can never be completely certain that a given theory is consistent. In fact, it is somewhat unclear what it even means to know that a given theory is consistent. If to "know" something means to have a proof of it, you must specify in which formal system you want a proof. Suppose that we have a proof in system $G$ that system $F$ is consistent. If we want to trust this proof, we should want system $G$ to be consistent. However, in order to "know" that system $G$ is consistent, we must have a proof in some other formal system $H$ that $G$ is consistent. See Lewis Carroll's dialogue "What the Tortoise Said to Achilles" to find out where this rabbit hole leads.

Perhaps you might want a system to be able to prove its own consistency. However, since everything is provable in an inconsistent theory, such a consistency proof would be meaningless, since any inconsistent theory can prove its own consistency. In fact, Gödel's Second Incompleteness Theorem tells us that any consistent theory that can formalize "enough" elementary arithmetic cannot prove its own consistency. So, such a consistency proof would be bad news; if a sufficiently strong system proves its own consistency, then it must be inconsistent.


You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .