[FOM] Proof assistants and conjectures

[Timothy Y. Chow]

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.

Tim