Can there be a problem for which we can prove there's a polynomial time algorithm and can prove that can't prove an algorithm is such? For a fiction story i imagined the following situation: there'd be a problem whose complexity depends on a natural number, for which a superpolynomial algorithm is known. Then a non-constructive proof is found that asserts there exists a polynomial algorithm for it. And then it is proved that given such an algorithm, it is impossible to prove that it works.
Is this situation known to be possible/impossible to happen? Has it ever happened / is there any known example of such example (even if it's an artificial problem designed to satisfy these conditions)?
 A: Part I: There probably aren't historical examples.
Imagine an $\mathsf{NP}$-complete problem $Q$ with at most one reasonable polynomial-time algorithm, $A$.  If ZFC fails to prove that $A$ solves $Q$, then $\mathsf{P}=\mathsf{NP}$ is independent of (unprovable from) ZFC.
In section 3.1 of this paper Scott Aaronson analyzes this possibility quite extensively; he ultimately concludes that such a fact would be (1) unprecedented (2) far beyond known techniques of proof and (3) very unlikely.  (Fun fact: such a circumstance would leave $\mathsf{NP}$ not much harder than $\mathsf{P}$.)
Now, I made some strong assumptions to conclude that $\mathsf{P}=\mathsf{NP}$ is unprovable.  For example, there are still hard (superpolynomial-time-requiring) problems that are not $\mathsf{NP}$-complete.  Or one can imagine an $\mathsf{NP}$-complete problem with many candidate solutions from $\mathsf{P}$, a few of which ZFC cannot prove to be actual solutions.  Or

then it is proved that given such an algorithm, it is impossible to prove that it works.

might describe a proof sketch: a description of how to turn a description of $A$ into a proof that "ZFC cannot prove $A$ solves $Q$," but which uses different axioms of ZFC depending on $A$, and so cannot prove "for any polynomial-time $A$, ZFC cannot prove the statement '$A$ solves $Q$'".
But if a problem of that sort had already come up, I think Aaronson would have mentioned it.
Part II: An artificial example
It turns out that the use of $\mathsf{P}$ in your problem is a red herring.
To begin, note that ZFC is not known consistent; moreover this likely cannot be known.  This is a separate question from whether proofs that ZFC is consistent exist: if ZFC is in fact inconsistent, then such a proof does exist.
Moreover: if ZFC is inconsistent, then ZFC proves any true (and any false!) fact.  So the statement it is proved that given such an algorithm, it is impossible to prove that it works probably omits some qualifiers.  (It must omit some qualifiers if, as the mathematical community believes, ZFC is consistent.)  A reasonable reduction would be: it is proved that, given such an algorithm and assuming ZFC consistent, then it is impossible to prove from ZFC that the algorithm works.
Finally, recall from the proof of Gödel's incompleteness theorem that natural numbers can encode ZFC proofs.
Now consider the following problem:

Check the input number to see if it is the smallest number that encodes a proof that ZFC is inconsistent.  Return $1$ if so; else return $0$.

I call this "problem $\Omega$."
One can "unravel" Gödel's proof to find a computer program $A$ that performs such a check.  Since each number encodes at most a finite-length proof, that computer program always halts, although it might take a long time to do so.  $A$ is your superpolynomial algorithm solving $\Omega$.
If ZFC is assumed consistent, then $A(n)=0$ for all $n$; and the computer program "return $0$" is clearly in $\mathsf{P}$.  Otherwise, $A(n)=0$ for all-but-one $n$ (say, $n_d$), and the program "if the input is $n_d$, return $1$, else return $0$" is also in $\mathsf{P}$.  This paragraph is your nonconstructive proof that there is a polynomial-time algorithm solving $\Omega$.
But which algorithm solves $\Omega$ is not provable from ZFC, because the consistency of ZFC is unprovable from ZFC.
Wait!  That's not quite right: if ZFC is inconsistent, then we can prove that the correct algorithm is in fact correct (because we can prove that any algorithm is correct).  The correct statement is:

Gödel's incompleteness theorem combined with the definition of $A$ proves:

if (1) ZFC holds and (2) ZFC is consistent, then ZFC cannot prove which polynomial-time algorithm solves $\Omega$.


But that is the reduction I mentioned at the beginning of this section, so we're done.
