[FOM] Proof assistants and conjectures

[Roger Bishop Jones]

On Monday 05 January 2009 04:37:39 Timothy Y. Chow wrote:
> For the most popular proof assistants, has there has been any systematic
> effort to compile databases of conjectures as well as of theorems?

There is a list of "The Hundred greatest theorems" at:

http://personal.stevens.edu/~nkahl/Top100Theorems.html

There is a page devoted to tracking formal proofs of these theorems at:

http://www.cs.ru.nl/~freek/100/index.html

This tracks progress in proving the "100 theorems" by eight proof assistants.
These are typically formal proofs concocted by people using software which 
aids and abets construction of the proof and ensures its correctness..
I don't think any two of the 8 participant provers accept the same notation, 
and this is the principle difficulty with the provision of a standardised 
list of theorems.  Four of the proof tools have an online list of the 
theorems so you can compare the notations.(and sometimes see the proofs or 
proof scripts). 

The situation is exacerbated by the fact that most things proven by such proof 
assistants depend for their statement and proof on extensive libraries of 
prior definitions and theorems.  Even if the notation were translated (which 
often will be straightforward) the lack of uniformity in the libraries would 
be an impediment to standardisation of the statement of the theorems.

This is still an advancing research effort which is well short of where we 
would like it to be, so there is no prospect at present of stabilisation.

The situation is different in automatic theorem provers, particularly for 
first order logic, where such lists are available.

Roger Jones