[FOM] Proof assistants and conjectures

[Timothy Y. Chow]

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

Tim