 The talk above of “every gap being filled in” in the transition to an ideal proof glosses over the fact that the notion of a “gap” in a proof is itself in need of further clarification. For one thing, the most straightforward way of defining a proof gap—as given below—is only applicable to fully formal systems.