I want to start out by two examples:

1. Graham's problem is to decide whether a given edge-coloring (with two colors) of the complete graph on vertices $\lbrace-1,+1\rbrace^n$ contains a planar $K_4$ colored with just one color. Graham's result is that such a $K_4$ exists provided $n$ is large enough, larger than some integer $N$.

Recently, I learned that the integer $N$ determined by Graham's problem is known to lie between $13$ and $F^{7}(12)$, which is called Graham's number, a number which beats any imagination and according to Wikipedia is practically incomprehensible. Some consider it to be the largest number which was ever used in a serious mathematical argument.

One way of looking at this is the following: Graham's problem of deciding whether for given $n$ and given coloring such a planar $K_4$ exists takes constant time. Indeed, if $n$ is small you have to look, if $n$ is large you are done. However, this takes polynomial time (check all four-tuples of vertices) for all practical purposes (assuming that $N$ is close to its upper bound).

I am sure someone can now cook up an algorithm which needs exponential time for all practical purposes but constant or polynomial time in general.

2. I also learned that the best proof of Szemerédi's regularity lemma yields a bound on a certain integer $n(\varepsilon)$ which is the $\log(1/\varepsilon^5)$́-iteration of the exponential function applied to $1$. This bound seems ridiculous in the sense that it does not even allow for interesting applications of this result (say with $\varepsilon=10^{-6}$) to networks like the internet, neural networks or even anything practically thinkable. At this point, this is only an upper bound, but Timothy Gowers showed that $\log(1/\varepsilon)$-iterations are necessary.

Again, it seems that one could cook up reasonable algorithmic problems which have solutions which are polynomial time but practically useless. Maybe one can do better in concrete cases, but this then needs additional input.

Coming closer to the question, what if finally $P=NP$ holds, but the proof involves something like the existence of a solution to Graham's problem or an application of Szemerédi's regularity lemma, so that finally the bounds of the polynomial time algorithm are for some reason so poor that nobody even wants to construct it explicitly. Maybe the bounds are exponential for all practical purposes, but still polynomial.

I often heard the argument that once a polynomial solution for a reasonable problem is found, further research has also produced practicable polynomial time algorithms. At least for Graham's problem this seems to fail miserably so far.

Question: Is there any theoretical evidence for this?

Now, maybe a bit provocative:

Question: Why do we think that $P\neq NP$ is necessarily important?

I know that $P$ vs. $NP$ is important for theoretical and conceptional reasons, but what if finally $P=NP$ holds but no effective proof can be found. I guess this wouldn't change much.