Why theorem proving is hard?

Question

Every time I ask why most people think that P ≠ NP, I get a response like "because theorem proving is harder than proof checking".

From this, I understand that proving theorems is hard. But why is this? In fact, it is known that a theorem, in mathematics, is a statement that has been proved on the basis of previously established statements. So a not proven theorem would not be called a theorem, would it? I mean, a theorem is easy to prove because it is defined to be so and people call it theorem because they know how to prove it, no? If we were talking about conjectures, I would have not asked this question.

When I was looking, I found this paper: Cook, Stephen (1971). "The complexity of theorem proving procedures". Proceedings of the Third Annual ACM Symposium on Theory of Computing. pp. 151–158. But this seems to confuse me furthermore.

I am sure I am missing something (maybe some obvious one). Would you please clarify this?

Answer 1

So a not proven theorem would not be called a theorem

No, it's usually called a proposition, or a conjecture.

I mean, a theorem is easy to prove because it is defined to be so and people call it theorem because they know how to prove it, no?

Just because you know a proof exists doesn't mean that you can efficiently find that proof.

From this, I understand that proving theorems is hard

The thing is, there is no mathematical evidence that it's hard, other than the repeated failures of people to prove that it's easy. But of course, the failures of people to prove that it's hard acts as evidence that it's easy.

When people say that proving theorems is harder than checking them, they are speaking from intuition. From a complexity theory standpoint, there is no evidence that proving theorems is harder than verifying them. If there were, we would be able to resolve $P$ vs $NP$. Any guesses one way to the other are just that, guesses.

There is, however, an analogy, from computability theory.

When people are talking about proving versus checking for $P$ vs $NP$, they usually mean things like SAT or Constructive Propositional Logic, or other such systems with no quantifiers, or restricted quantifiers. But if we extend proofs to include predicate logic, with $\forall$ and $\exists$, then we have a firm result: checking proofs of these is decidable, and generating such proofs is undecidable. This is a basic consequence of the undecidability of the halting problem.