Almost all of this paper is dedicated to discussing whether or not computers can be "creative". Then it mentions in passing that computer-discovered theorems ma

Almost all of this paper is dedicated to discussing whether or not computers can be "creative". Then it mentions in passing that computer-discovered theorems may be long and impenetrable (even if they are profound). I guess I was expecting some attempted concrete task definitions of creativity, such as "finds and proves statements with many useful implications and applications", and discussion of how well existing theorem provers do at those kinds of tasks. But instead of the "how might we achieve this, and what will change?" paper I was hoping for, this is more of an "are we special?" paper.