The whole point of that paper is to show that it's possible in principle. Now people (and AIs) can think of better algorithms, etc.

Regarding elegance, take a look at Graham's number. It was not some meaningful constant - it's just a big-ass number which could be used in existence proof. Human mathematicians have been using this approach for quite some time, it's not really AI doing things odd