[strangestchild]

I think this is very dependent on the area of maths. In applied mathematics, obviously simulation is of huge importance; and in very fundamental pure maths the language is close enough to formal logic to make it easier to apply computer-aided proof.

But in very pure disciplines which rely on several layers of supporting definitions and theorems, there is little to be gained from numerical computation - but huge amounts of bootstrapping are still required before the computer can prove results of its own using logical manipulation.

To take a simple example, writing a computer program capable of proving that there are infinitely many primes - without embedding so much domain knowledge in it as to render it useless - seems a pretty nontrivial task.

[Someone]

Nontrivial, but doable. See #11 in http://www.cs.ru.nl/~freek/100/

Also: http://us.metamath.org/mpegif/infpn.html

[fusiongyro]

I think it supports strangestchild's thesis that all five proofs from this page[1] would fit on a page and a half printed but the Coq proof (the only one I could find a download for from your list) is 825 lines of code.

[1]: http://primes.utm.edu/notes/proofs/infinite/

[Someone]

You can easily fit all of them on one page, as long as you build enough scaffolding theorems to get there.

I am not that familiar with the field, but http://us.metamath.org/mpegif/infpnlem2.html fits on one page. If you fully expand the proofs of each subclause, I don't know how long it is, but it won't fit on a page. You will get through to the 'bloody obvious', though, with such things as http://us.metamath.org/mpegif/syl.html "if A implies B and B implies C, then A implies C", which this system proofs from http://us.metamath.org/mpegif/a1i.html "if A is true, then anything implies it" and http://us.metamath.org/mpegif/ax-mp.html "if A is true and A implies B, then B is true"

[fusiongyro]

Yes, well, I suppose I could fit all of Firefox on one page as long as you only look at the main() function and not any of the functions that lead up to it. But that doesn't really tell you much about Firefox, does it? And the fact that there are primitives like pthread_create() and pow() underneath at sufficiently low level doesn't really say much either.

[Someone]

Yes, but like that 'main', all those short proofs are full of holes. For example, Euclid assumes readers know what he means when he talks of prime numbers, what multiplication and division are, how they work. For example, given p and q, how many different r's can there be such that r=p/q? Given n and p>1, how do we know p does not divide n * p + 1? Is it always possible to write a number as a product of primes?

Each of these may lead to new branches of mathematics in which Euclid's theorem does not hold or only holds in a restricted way.

I am not denying that writing automated proofs is a nuisance, but you also get more in the process. For proofs like this, barely anything more, but surely, the promise is there.