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