I don't know. You could also enumerate all proofs and check whether P is a proof that a turing machine T solves SAT in polytime (if P=NP, this requires a finite

I don't know. You could also enumerate all proofs and check whether P is a proof that a turing machine T solves SAT in polytime (if P=NP, this requires a finite number of steps ^) and then run T. ^ It would be funny though if P=NP, but for no turing machine exists a proof that it solves SAT. This would have to be ruled out for the algorithm to work.