It seems like there is a sense in which a Turing machine that demonstrates P=NP could be said to "accidentally" exist. I'm wondering the extent to which the possibility of such machines is the main reason P not equal to NP is so hard to prove. A priori can such machines exist, or are there heuristic or known reasons they can't?

By a Turing machine that accidentally solves P=NP, I mean a Turing machine that solves an NP-complete problem, say 3-SAT, in polynomial time. But its description might bear no logical or discernible relation to 3-SAT. To make this precise, maybe the right definition of an accidental solution is that it's not provable that the machine is a solution, even though one could observe empirically that it is (because it would be).

This would be analogous to observing empirically that a solution to 3-SAT happens to be encoded in the digits of pi starting at some digit (under some natural enumeration of all 3-SAT inputs and with pi written in base 2), or in the digits of some other irrational number whose digits can be computed in polynomial time.

If the existence of accidental solutions is consistent with ZFC, say, then P not equal to NP couldn't be proven. If this is in fact one of the things that makes P versus NP difficult, does it make sense to consider a variant of the P versus NP problem that restricts P not just to Turing machines that accept certain languages in polynomial time, but also to ones for which this is provable? Does this make the problem any easier?

Lines of thinking like this might be common knowledge to complexity theorists, but I haven't seen it expressed in writing.

This question is a little reminiscent of this MO question about the Goldbach conjecture.