I suspect if you created some kind of a graph between related theorems, you could identify the interesting ones by how many edges a particular node has, or by w

I suspect if you created some kind of a graph between related theorems, you could identify the interesting ones by how many edges a particular node has, or by whether or not it is a part of a previously unknown shortcut between such nodes. I also suspect some form of this has already been done. I know this problem has been identified and there are all sorts of ideas to try to come up with a criteria for “interesting”. Don’t know what you call that area of research or what the latest is/am not a professional mathematician. But yeah, a world in which everyone becomes dependent on computer generated maps to parse through seas of computer generated jargon seems less like a world where people do math and more like a world where people do mathematically informed seances. Finding isomorphisms might also be misleading. Formalizing some set of assumptions for a theorem might identify non existent similarities that have more to do with using the same meta language to formalize things rather than the intended meaning of some of the theorems. Again, pretty sure these issues are well understood, and people smarter than me are doing things to mitigate them, but I think there’s a real big problem here related to translating machine created discoveries into a meta language a computer can make sense of and then back into a language humans can understand better and verify without relying on the machine.