| No. That wouldn't be sufficient. Here's why. 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. |