The other trick could be bootstrapping through mathlib.

As you said brute forcing the search space as the starting procedure would take way too long for the AI to build intuition.

But if we could give it a million or so lemmas of human math, that would be a great starting point.