Imagine that I built a machine and told you, "Press this button here. If P=NP, the lamp will turn on. If P!=NP, the lamp will not turn on." What would you make of it?

So what if I opened up the machine, and showed you all the components, would that convince you?

I think you'd only be convinced, if:

1. We could agree on some basic axioms of how the basic components of the machine operates.

2. From those axioms, I could prove the proposition that, for a machine of this design, the lamp will turn on if and only if P=NP.

I think that, one day, somebody WILL construct a formally verified silicon system capable of proving the four color theorem. (Putting aside the issue of unreliable logic gates.) But I don't think it will be in some high-level system like Coq, because there are so many layers of abstraction we would have to formally verify. I think it's more likely that the logic would be implemented directly in silicon.