In theory a proof could show that such an algorithm must exist without producing the algorithm itself. Though that's not what this linked paper tries to do.
In fact if there was a non-constructive proof, we would already know a polynomial time algorithm for solving any NP problem: just iterate over all program lengths (from 1 to infinity) and then iterate over all programs of that length n, running each for n steps. If one of the guesses produces the correct answer (which it must if P = NP), we have a polynomial time algorithm! Wild, huh?
This finds a certificate for positive instances, but without a complexity bound can this be made to solve the decision problem in the presence of negative instances?
I had to look this up since it’s been a while, but looks like no - this is not a full solution. It correctly accepts the positive instances in polynomial time but no algorithm is known that would fully decide all instances in polynomial time.