LEAN and other tools verify from what do know -- at least stepwise. Anything that deviates from these things should stick out. I suppose some million line LEAN program may have embedded within it something that is novel and not readily apparent, but I imagine truly novel approaches should stick out like a sore thumb.
Could AI create a novel set of axioms (a new math) from which things like RH become a by product? I think that would be hard to miss.
Dozens of agents probably already invented it, but they were given ephemeral containers where noone ever looked or they only wrote it in direct CPU instructions.
I would really like to see an AI invent a new set of (consistent) axioms from which a whole slew of new problems and solutions arise. Something akin to Euclidean geometry, but for a whole new landscape of theorems.