Why does being a compressed corpus of knowledge mean it can't discover things? What if it has knowledge of techniques to discover proofs?

It does and that's what's happening.