There is actually quite a bit that can be mechanized in proof finding. Up to and including completely deriving a proof mechanically. And I don't just mean that automatic theorem provers exist. A decent amount of a proof is highly constrained. In my experience, it is not uncommon for people to struggle with even these extremely constrained proof steps. While writing a "good" proof (i.e. one which is concise yet enlightening) might be a bit of an art, writing a proof is much less so. There isn't a concept of a "valid novel" or a "valid next sentence" in writing. There certainly is for proof writing. Writing a proof is closer to designing a bridge. There are better and worse designs for bridge that nevertheless function (e.g. a worse design might be more expensive, labor intensive, and/or aesthetically unpleasing but still work), and there are designs that don't work at all.

To give an example of the kind of thing I'm talking about, consider the following more positive rendition of the infinitude of primes: For any finite set of primes, there exists a prime not in that set. I can produce the following proof skeleton completely mechanically from the form of the proposition even if I didn't know what "finite", "set", or "prime" meant. Proof skeleton: "Assume we're given a finite set $S$. Let $p(S)$ be (...). $p(S)$ is prime because (...). Assuming $p(S)$ is in $S$ leads to the contradiction (...). Q.E.D." Now it still requires some cleverness to fill in the blanks, mostly the one defining $p(S)$ because that step is largely unconstrained. Nevertheless, at a low level in contrast to "for the most part it isn't the case that whenever you see X, you know you'll need a proof of type Y", it actually is the case that there are only a few relevant rules at any step of a proof, though some, like cut, have an unbounded number of largely unguided instantiations.

It is also the case that the need for insight is often oversold. Many results about sums of binomial coefficients and closely related combinatorial identities have clever proofs involving insights and analogies. However, virtually all "textbook" identities of this form fall within the purview of a decision procedure which can not only immediately tell you whether the identity holds but also produce a certificate letting you easily verify it. Being aware of such decision procedures, i.e. when insight is not required, is also very useful. Indeed, the fact that there are two commonly known decision procedures for deciding the equality of polynomials (over $\mathbb Q$, say), namely 1) writing both in the normal form $\sum_{k=0}^n a_k x^k$, or 2) comparing the polynomials at a number of points greater than their degree, means we usually don't see spelled out proofs of polynomial equality.

Derek Elkins‭, I agree that there are some ways that writing a proof is more like designing a bridge than writing a novel (and some ways that it is like neither). And yes, there are skeletons that get reused and are good to know. The sorts of questions I'm objecting to are not questions like, ‘What types of proof structures could be used to prove the infinitude of primes?’ but rather, ‘How did this author know to use $p(S) = 1 + \prod S$?’ followed by, ‘I'm not interested in an explanation of why $p(S)$ is prime; what I want to know is how someone got the idea to use that definition at all!’ Are you making the case that there's a better answer to that question than ‘experience, persistence, and luck’? It's great that in some circumstances, decision procedures can substitute for insight; but even in those circumstances, in the context of reviewing a proof in a textbook, unless that decision procedure is what's being taught, do you think that's a useful answer to the question?

I haven't downvoted (or upvoted) this meta answer, but I haven't yet completely decided how I feel. On the one hand, I think in practice there are indeed a lot of bad questions of the form discussed. On the other hand, I am making the case that there are often better answers than "experience, persistence, and luck" especially across the whole class of questions of this type. As I've stated, I've often seen questions asked about the parts of a proof that are completely mechanical, e.g. many people learning proofs would struggle making the proof skeleton I illustrated while having no problem filling it in. That is, they don't understand what they need to do to have a proof. A bit more softly, a common general hang-up I've seen for people starting out in proofs is that they don't use definitions. Of course, there is also advice specific to fields, e.g. using a generating function or manipulating the problem into a form suitable for a decision procedure.