On the provability of P versus NP First of all, my understanding on Gödel's incompleteness theorem (and formal logic in general) is very naive, also is my knowledge on theoretical computer science (meaning only one graduate course taken while I'm still an undergraduate), so this question may be very naive.

As far as I could find, the provability of P versus NP is an open problem.

Now:


Gödel's first incompleness theorem states that there may be statements that are true but not provable nor disprovable.
If a polynomial solution is found for an NP-complete problem, it proves that P = NP.


So, suppose that P=NP is not provable:
This means that no example of a polynomial solution for an NP-complete problem can be found (otherwise, this would be a proof).
But if no example of a polynomial solution for an NP-complete problem can be found, this means that P=NP is false (proving it, meaning the statement is provable), which leads to a contradiction, therefore P=NP should be provable.

This sounds like a proof of the provability of P=NP to me, but I think it's extremely likely that it is due to my lack of understanding of the logic topics involved. Could anyone please help me understand what is wrong with this?
If P=NP, there must be polynomial-time algorithms for NP-complete problems.  However, there might not be any algorithm that provably solves an NP-complete problem and provably runs in polynomial time.