The Gödelian insight is all that we need
It's not necessary to see the consistency of an entire formal system. The ability to pass from one formal system to the Gödel sentence of that formal system is enough.
This kind of Gödelian insight, which is not captured by formal rules, is characteristic of mathematical insight and is non-algorithmic.
Roger Penrose (1990).