One hesitation I have with this idea is that proofs themselves can be modeled as mathematical objects. So if you have a machine which can construct examples then we just view the proof as an example, and it should be good at constructing them.

Maybe this is naive.