6 added 820 characters in body

Maybe I should start by saying that the quote from Cook is convincing. If a useful polynomial time algorithm for NP complete problem will be found then a computer will be able to give us quickly proofs for theorems (admitting not too long proofs) that we are interested to prove (and may eventually prove), as well as much harder questions that we are uninterested to prove and it seems that we will never be able to prove. (Is the shortest proof of FLT has an even number of characters?) This automatic ability to prove may lead to much more understanding of mathematical theorems and phenomena. We can explore if a specific direction to a proof works, try all sort of lemmas. explore surprising connections, etc. This picture gives good reason to believe that $P \ne NP$ but there are even better reasons for that.

5 added 783 characters in body

There are various reasons to believe that $NP \ne P$ and indeed one reason is that various tasks that look intractable will immediately look much easier compared to what we experience and expect. The connection with proving specific mathematical theorems looks artificial from various reasons. Usually, to transform a mathematical task into a decision problem to which the NP=?P problem is relevant we need to add a statement like "Is there a proof for RH with less than n pages". This addition makes the original problem much harder. Probably We have a proof for FLT but probably we will never be able to answer the question "what is the smallest number of characters in a proof of FLT?". But Fortunately we do have a proof for FLTfind the later question uninteresting. So overall Cook's statement can be seen as a provocative agument for why $NP \ne P$, which has some merit, But I dont think it offers any useful connection,

One argument against the connection of real life mathematical proofs and the NP/P gap goes as follows. The NP/P problem is about the effort needed to find a proof compared to the effort needed to verify a proof. Now think about ourselves as computational devices and about this gap for cases of proven theorems. Try to estimate the amount of effort that it takes you to verify a proof which capture n journal pages (or n words) compared to finding such a proof. Is it superlinear in n? more than Quadratic in n? This gap (sometimes referred to as the creativity gap) does not seem similar to the gap between finding a proof and verifying a proof in the NP/P theory (say, the gap between finding a hamiltonian cycle in a large graph or verifying that a certain list of vertices and edges form a Hamiltonian cycle.) We can also talk bout the human effort needed to produce an n-page (or n characters) proof. This effot is on average (for cases of success) probably monotone in n, perhaps superlinear in n but there is no reason to expect it to be exponential in n.

Just to make the main point clear: Deciding mathematical problems including famous ones appears to be by far easier than solving NP-complete problems, and therefore the $NP \ne P$ by itself seems to offer little explanation for the difficulty in solving mathematical problems, . But computational complexity insights do give some understanding of this difficulty.

Does the fact that there are mathematical statements that are undecidable give some explanation why some mathematical conjectures are so hard to prove? (Well, it gives some indirect explanation of a sort, but not a real useful connection.)

It is an interesting question why proving mathematical conjectures does not seem to be computationally intractable at least for surprisingly many cases where people succeeded. (Also undecidability enters the scene rather rarely.) I am not aware of a very good answer to this question. It may have something to do with what we regard as "interesting" in mathematics, to the nature of mathematical understanding, and to the highly structured nature of mathematical problems.

There are various reasons to believe that $NP \ne P$ and indeed one reason is that various tasks that look intractable will immediately look much easier compared to what we experience and expect. The connection with proving specific mathematical theorems looks artificial from various reasons. Usually, to transform a mathematical task into a decision problem to which the NP=?P problem is relevant we need to add a statement like "Is there a proof for RH with less than n pages". This addition makes the original problem much harder. Probably we will never be able to answer the question "what is the smallest number of characters in a proof of FLT?". But we do have a proof for FLT. So overall Cook's statement can be seen as a provocative agument for why $NP \ne P$, which has some merit, But I dont think it offers any useful connection,

One argument against the connection of real life mathematical proofs and the NP/P gap goes as follows. The NP/P problem is about the effort needed to find a proof compared to the effort needed to verify a proof. Now think about ourselves as computational devices and about this gap for cases of proven theorems. Try to estimate the amount of effort that it takes you to verify a proof which capture n journal pages (or n words) compared to finding such a proof. Is it superlinear in n? more than Quadratic in n? This gap (sometimes referred to as the creativity gap) does not seem similar to the gap between finding a proof and verifying a proof in the NP/P theory (say, the gap between finding a hamiltonian cycle in a large graph or verifying that a certain list of vertices and edges form a Hamiltonian cycle.)

Just to make the main point clear: Deciding mathematical problems including famous ones appears to be by far easier than solving NP-complete problems, and therefore the $NP \ne P$ by itself seems to offer little explanation for the difficulty in solving mathematical problems, But computational complexity insights do give some understanding of this difficulty.