Finding Cantor’s proof that there are transcendental numbers

I’ve just posted a question at Mathoverflow challenging people to come up with examples of proofs that appear to require a sort of “cognitive leap” that humans are surprisingly good at and that it is hard to imagine computers ever being capable of. I don’t myself believe that there is some fundamental way in which humans are better at mathematics than computers are (or rather, could ever be). So this is the first of what may turn into a series, if I have time, of posts in which I shall try to demonstrate that examples that have been suggested are of proofs that a computer program could in principle find too. (Many of the examples suggested are in areas where I have absolutely no hope of doing this: I’m not going to be able to tell you how a computer could have invented Thom’s work on cobordism, for instance.)

In this post I want to tackle a proof that was a pretty radical departure when it first came out: Cantor’s indirect proof of the existence of transcendental numbers.