i agree that the task of actually searching for a valid proof or counterexample of some hypthosesis (rather than verifying a given purported proof is correct or

i agree that the task of actually searching for a valid proof or counterexample of some hypthosesis (rather than verifying a given purported proof is correct or not with respect to some known axioms/theorems etc) relies on an awfully large amount of intuition & knowledge of standard heuristic "tricks" that might be applied to guide the search. i only took pure math to undergrad level, but sitting in lectures and having a particular proof explained was often fairly frustrating ("why on earth would we think of applying that particular trick there?" "where on earth did that idea come from?") from the perspective of thinking how you (or a machine) might go about methodically discovering a proof for yourself.