I don’t think that’s really what Occam’s razor says. If one’s goal is to use ML stuff to try to produce new useful theorems, it seems useful towards that goal

I don’t think that’s really what Occam’s razor says. If one’s goal is to use ML stuff to try to produce new useful theorems, it seems useful towards that goal to come up with a numeric heuristic for how useful a new theorem is. And, stating such a heuristic explicitly seems reasonable. Just because the heuristic that they state, which they expect to be a crucial component of what makes a theorem useful to prove in a given context, isn’t particularly surprising, doesn’t make it not worth saying. to elaborate on “isn’t particularly surprising” : if you asked many other people to come up with heuristics for the usefulness of a new potential theorem, I imagine many of the answers you would get (counting multiplicity if multiple people give identical answers) would be fairly similar. Even if a hypothesis is an obvious-to-consider hypothesis, if one wants to talk about it, it is worth stating what it is first.