[FOM] Proof assistants and conjectures
Timothy Y. Chow
tchow at alum.mit.edu
Mon Jan 12 11:31:47 EST 2009
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).
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.
More information about the FOM