[FOM] Proof assistants and conjectures

[Tjark Weber]

On Wed, 2009-01-07 at 15:36 -0500, Timothy Y. Chow wrote:
> 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."

This is typically not a big issue.  The language/notation of proof
assistants is fairly close to standard mathematical notation, and
conjectures (e.g., the Riemann hypothesis) are typically fairly short
statements.  Occasionally the fact that some proof assistants are not
based on ZF set theory may obscure matters, but in general it is "easy"
to see whether a formal statement correctly captures, say, the Riemann
hypothesis.  Much easier at least than seeing whether a proposed proof
of the Riemann hypothesis is correct.

> 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.

While there might be some value in having a collection of formal
conjectures, these are usually generated "on the fly" when someone
embarks on a formal proof -- simply because there's typically not much
insight gained from formalizing just a conjecture (without proof).

On the other hand, when formalizing a conjecture gets more complicated,
there's often more than one way to do it -- and which (equivalent)
approach is superior may become clear only after you've done a proof.
So it might be cumbersome for people to have to work with a prematurely
chosen "official" version.

Regards,
Tjark