zo'n programma's bestaan ook al een hele tijd. Graffiti http://math.uh.edu/~clarson/graffiti.html heeft een hele boel leuke conjectures in de grafentheorie ontdekt.

@Johan:

zo'n grote bewijzen zijn nog heel ver boven de capaciteit van de huidige systemen. Het was een hele verwezenlijking toen het Mizar project, dat de bedoeling heeft op termijn om de gehele wiskunde in hun systeem te krijgen, een paar jaar geleden erin slaagde om de Jordan curve stelling te bewijzen.

The proof works as follows:

- we work towards a contradiction by showing that from the assumption that we have a list holding precisely the primes it follows that 1 is prime; once we have that we're done, as clearly 1 is not a prime

- actually, it is sufficient that this list holds all the primes (so there also might be non-primes in it); this is the "assert (X:=...)" step in the proof script

- as a first step we are going to show that the product of this list plus 1 is prime

- for this it is sufficient that any prime q that divides this product plus 1 has a square that is bigger than that product plus 1

- we do this by contradiction by showing that such a q has to be 1, so cannot be prime after all

- Coq shows that this q is 1 by the magic of "eauto with *"; when you investigate how this works, it turns out that it shows that q divides 1; that is the case because it divides the product of the list (it being a prime) as well as that product plus 1 (that was how q was chosen)

- so now we know that the product of the list plus 1 is prime; from this we then deduce that 1 is prime (our goal) by showing that that product plus 1 actually is 1. Again that happens by showing that it divides 1, by showing that it both divides the product of the list (it having shown to be prime) as well as the product of the list plus 1 (because that is itself).

- so now we have that 1 is prime, the contradiction that we were looking for, and we're done