[Jimmy]

Naturally, the first step for AI mathematics would be generating proofs of theorems that humans have already deemed interesting, rather than the AI generating entirely new research directions all by itself.

Certainly it’s an interesting problem to think about how one would formalize the notion of interesting/important mathematics. But it’s not necessary to solve that problem in order for AI to start having a big impact on how mathematics is done.

[IIAOPSW]

This implies that the discovery of math and the existence of math ultimately comes down to human taste and can only be learned by studying humans. I'd like to think human reasoning is a crude approximation to mathematics in all its glorious purity, not the other way around.