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