[FOM] Proof assistants and conjectures
Timothy Y. Chow
tchow at alum.mit.edu
Wed Jan 7 15:36:16 EST 2009
On Wed, 7 Jan 2009, Gergely Buday wrote:
> Different theorem provers can have different underlying logic and even
> if the logic is similar the concrete syntax might be different.
The problem I raised exists even if you stick to one particular theorem
prover. I announce a proof of the Riemann hypothesis and exhibit a proof
in Coq. You look at it and say, "That's not the Riemann hypothesis; what
you've proved is some other statement." Me: "It most certainly *is* the
Riemann hypothesis." "Is not." "Is too."
There cannot be any strictly formal solution to this problem, but it can
be partially addressed by having an official *formal* version of a
conjecture in place before anyone has any clue how to prove it.
More information about the FOM