The problem of generating inductive invariants for parameterized or infinite-state systems has attracted continuous interest over the last several decades. The fact that the invariants require quantifiers presents challenges both in heuristically synthesizing them and in verifying them. Many approaches attempt to transform the synthesis problem in an incomplete way to finding finite-state or quantifier-free invariants, or attempt to generalize from proofs of finite instances in some way. Other methods go at the problem more directly, using some form of inductive synthesis (i.e., synthesis from examples). We will discuss some recent progress in this area and consider whether proof-based heuristics might also have a role to play in the problem synthesizing quantified invariants.