[FOM] Proof assistants and conjectures

[Steven Ericsson-Zenith]

On Jan 7, 2009, at 12:25 PM, Timothy Y. Chow wrote:

> It's clear from some of the responses that my question was not  
> understood
> by everyone, so let me try again:
>
> I wrote:
>>> For the most popular proof assistants, has there has been any
>>> systematic effort to compile databases of conjectures as well as of
>>> theorems?
>
> The following emphasis may help people parse my question.
>
> Has there been any systematic effort to compile databases of  
> *CONJECTURES*?

I'm afraid that this does not help much, since generally the basis of  
conjecture is not itself uniform. To suggest a uniform basis to  
conjecture is to either make concrete the status quo or anticipate all  
future work.

Perhaps you mean simply to limit the scope of these conjectures to  
specified formal systems in the most popular proof assistants. I could  
have been misled by your desire to "prevent different pioneers from  
developing overly idiosyncratic dialects." But if this is the case,  
then your database seems unlikely to serve the true pioneer.

Sincerely,
Steven

--
	Dr. Steven Ericsson-Zenith
	Institute for Advanced Science & Engineering
	http://iase.info
	http://senses.info