In the proof assistants I'm familiar with, such as Lean and Coq, you can write tactics which generate proofs for a goal and potentially produce more subgoals. However there isn't a "one size fits all" tactic for these gaps. One area that is being explored is ML for generating proofs, but training data is limited.