The Gödelian insight has already been formalised
Programs have been developed that can derive Gödel's theorems. The Gödelian insight has, in effect, been formalised.
Penrose neglects this possibility because he fails to distinguish between the formal system within which a Gödel sentence is proven and the system that does the proving.
Stewart Russell and Peter Norvig (1995).
Note: This came was originally articulated as an attack on Penrose's response to Boolos—see "The Gödelian insight is all that we need", Box 66. Also, see the "Does Gödel's theorem show that mathematical insight is not algorithmic?" arguments on this map.