[FOM] Proof assistants and conjectures
Timothy Y. Chow
tchow at alum.mit.edu
Sun Jan 4 23:37:39 EST 2009
For the most popular proof assistants, has there has been any systematic
effort to compile databases of conjectures as well as of theorems?
Here's a hypothetical scenario that illustrates the potential importance
of having "official" formal versions of conjectures. Someone claims to
have a proof of the Riemann hypothesis, and even claims that some standard
proof assistant has checked the proof. If the claimant is free to
formulate his or her own version of the Riemann hypothesis, then there
would still be the possibility for debate about whether the claimant's
formal theorem is, in fact, the Riemann hypothesis. This loophole could
be largely closed if there is a published, "official" version of the
Riemann hypothesis than any wannabe millionaire needs to prove.
I suppose one could argue that an official version could be produced on
the fly, as needed, so that there is no need to prepare them in advance.
However, from the point of view of knowledge management, it would seem
desirable to put down some stakes in the sand even in uncharted territory,
to prevent different pioneers from developing overly idiosyncratic
dialects that later turn out to be extremely difficult to translate
More information about the FOM