[FOM] Proof assistants and conjectures

[Timothy Y. Chow]

Tjark Weber wrote:
>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).

O.K.

It occurs to me now that in the specific case of the Riemann hypothesis, 
it is highly likely that it will be formalized before a proof is found, 
simply because RH is used as a hypothesis in so many theorems.  The same 
goes for a handful of other conjectures, such as P != NP, that are 
routinely assumed by workers in the field.  In these cases there may be no 
need to make any specific effort to formalize conjectures, since they will 
be formalized anyway in the course of formalizing theorems.

There is one other reason I can think of for formalizing conjectures, 
which is in support of conjectures for which prize money is offered.  
Formalizing the conjecture ahead of time could help forestall disputes 
about whether the conjecture has been proved.

Tim