Gödel’s proof

A recent opinion article (Nature, Aug 14) has an interesting retrospective look on Gödel’s proof, the 1958 secondhand description of Gödel’s 1931 finding that rules of logic for quoting axioms eg. substituting variables and formulating deductions are themselves mathematical operations – pretty much the same of todays object oriented programming where an object (as set of operations) is applied to another object eventually generating a new object. But what’s about his

astonishing discovery of true mathematical statements that could not possibly have a formal proof

Working currently on an analysis where there is basically not available model, no empirical expert knowledge on thresholds etc with extremely rare data, Gödel’s proof is a most painful insight.
There is also another aspect that came to my mind when reading the Nature essay. The author cites “How to solve it” without giving a reference to the classical text of George Polya (1945) known for

To be a good mathematician, or a good gambler, or good at anything, you must be a good guesser.

I have the 1988 edition on my book shelf. “How to solve it” is a much less theoretical than practical account that lays out an heuristical approach to solve mathematical and other problems

It is hard to have a good idea if we have little knowledge of the subject and impossible to have it if we have no knowledge.

Yea, yea.