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