I don't think the computer actually invented the proof.

Think of a computer playing chess. It does not "invent" new moves intelligently, it just does a brute force search on all possible future moves.

Much the same with a proof, it can scan all possible options until it finds a path from where started to where it needed to end. That is where the human input came in... "We need to start HERE and we want to see if we can find a mathematical path to X", where that mathematical path could be extremely complex. All we needed to teach it were the possible operations it can perform and what constitutes a desired outcome. It's kinda like evolution really (there's a branch of AI called "genetic algorythms", more below), it simply tries to do operation A, from there B, ....., from there Z. If Z (where Z could be millions of "moves" in the future) does not match some kind of "fitness criteria" (frequently used in AI) or is not a valid result, it disregards Z. Once it has tried all permutations of the "branch" of Y it disregards Y and tries another operation on X, and so on.

So one programs some "intelligent guesses" (heuristics, the fitness function, etc...) into it to make the process faster, but the result is it can "invent" a new proof for something (or confirm that there exists NO path from A to Z), but humans first needed to suspect there's something there.

Then again in genetic algorythms, what you do is define a fitness function once more (Itself something you can test iteratively to find the best one), but you generate a set of completely random "proofs". You then apply the fitness function to eliminate, say, 90% of the "weakest" candidates. You then "breed" the remaining proofs, you swap pieces between them, to produce a large number of "offspring", then make the fittest of those survive and breed, etc... Eventually you find that the proofs evolve into more and more valid candidates until you find a completely valid proof, or say a new algorythm that takes certain inputs and always gives you the desired outputs. I have written a genetic algorythm myself, it is fascinating to see in action..... millions of generations gradually moving towards the anwser you're looking for, often producing counter-intuitive and surprising, yet valid, results.

The problem with this is, of course, much like we have vestigial bits that are no longer useful to our function, the results of genetic algorythms have the same property. They could have 100 steps where 10 would do. As you say, they lack "elegance".