I don't know if there are too many problems that are in P but only "theoretically".
Actually there is a known class of problems that are in P, but only "theoretically"! But for very different reasons than what you are thining of.
See http://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theor... for a theorem that implies that certain types of graphs are characterized by a finite set of forbidden graphs that cannot be embedded in any form. (I'm being vague about "in any form" here, what I mean is that you can't do things like subdivide an edge and put a point in the middle then say, "Here! I changed it." More formally the forbidden subgraph can't be a minor of the main graph. See http://en.wikipedia.org/wiki/Minor_%28graph_theory%29 for an explanation of what a minor is.) For instance planar graphs cannot contain in any form 5 points that all connect to each other, nor two collections of 3 points that all connect to each other. (These are known as K5 and K3,3.) Any graph that does not contain these anywhere is planar.
It turns out a finite forbidden set of minors can always be tested in polynomial time. Therefore an class of graphs that meets the conditions for the Robertson-Seymour theorem has a polynomial time test.
Here is the catch. For many classes of graph we can prove that this polynomial time test exists. But we don't actually know what it is. Finding it requires enumerating the finite set of forbidden minors. But we have no way to figure out what they are. For graphs that can be embedded in the plane we know that there are just two. The projective plane turns out to have 138. As of 2004 I know that were nearly 240,000 known for the torus, and this list was not believed to be complete. According to http://www.cs.uvic.ca/~ruskey/Theses/WoodcockMScThesis.pdf there were theoretical algorithms that were O(n) and O(n^3), but nobody had ever implemented them and it was suspected that they would be too slow to use in practice. Moving on, consider the set of graphs that can be embedded in 3D without any knots. To the best of my knowledge nobody even has an exponential algorithm for that - yet we know that the problem must be in P.
So there you are. A whole family of problems, all of whom are known theoretically to have solutions in P, but for most of them we have no way to find said solutions, and even if we did find them they would likely be too slow to use in practice.
> For instance planar graphs cannot contain in any form 5 points that all connect to each other, nor two collections of 3 points that all connect to each other. (These are known as K5 and K3,3.)
Huh. I know this intuitively from doing those "try to connect the three houses to the three respurces without crossing any lines" kind of puzzles when I was younger—but I never made the connection that this kind of puzzle is basically the proof of the four-color theorem. My (puny) knowledge of topology has been made slightly more concrete. :)
but I never made the connection that this kind of puzzle is basically the proof of the four-color theorem.
Sorry, but the proof of the four-color theorem is much, much more difficult than the proof of this result. (Which is called Kuratowski's theorem and was proved in 1930.)
Actually there is a known class of problems that are in P, but only "theoretically"! But for very different reasons than what you are thining of.
See http://en.wikipedia.org/wiki/Robertson%E2%80%93Seymour_theor... for a theorem that implies that certain types of graphs are characterized by a finite set of forbidden graphs that cannot be embedded in any form. (I'm being vague about "in any form" here, what I mean is that you can't do things like subdivide an edge and put a point in the middle then say, "Here! I changed it." More formally the forbidden subgraph can't be a minor of the main graph. See http://en.wikipedia.org/wiki/Minor_%28graph_theory%29 for an explanation of what a minor is.) For instance planar graphs cannot contain in any form 5 points that all connect to each other, nor two collections of 3 points that all connect to each other. (These are known as K5 and K3,3.) Any graph that does not contain these anywhere is planar.
It turns out a finite forbidden set of minors can always be tested in polynomial time. Therefore an class of graphs that meets the conditions for the Robertson-Seymour theorem has a polynomial time test.
Here is the catch. For many classes of graph we can prove that this polynomial time test exists. But we don't actually know what it is. Finding it requires enumerating the finite set of forbidden minors. But we have no way to figure out what they are. For graphs that can be embedded in the plane we know that there are just two. The projective plane turns out to have 138. As of 2004 I know that were nearly 240,000 known for the torus, and this list was not believed to be complete. According to http://www.cs.uvic.ca/~ruskey/Theses/WoodcockMScThesis.pdf there were theoretical algorithms that were O(n) and O(n^3), but nobody had ever implemented them and it was suspected that they would be too slow to use in practice. Moving on, consider the set of graphs that can be embedded in 3D without any knots. To the best of my knowledge nobody even has an exponential algorithm for that - yet we know that the problem must be in P.
So there you are. A whole family of problems, all of whom are known theoretically to have solutions in P, but for most of them we have no way to find said solutions, and even if we did find them they would likely be too slow to use in practice.