Godel started with the liar paradox: "This statement is not true." But "true" is a rather difficult concept to define for axiomatic proof systems (see Tarski's undefinability theorem) so Godel modified it to the alternative "This statement is not provable." "Provable" is often used as a substitute for "true" in axiomatic proofs. This second statement, too, is a bit too vague for formal logic - what do you mean by "provable"? We have lots of different sets of axioms, lots of different rules of deduction. So Godel adds more detail: "This statement is not provable in the formal proof system Y." where "Y" stands for some set of axioms and deductive rules.
Now we can encode the formulas as numbers and the deductive rules as arithmetical relationships between them, so "provable in the formal proof system Y" becomes an arithmetical fact about numbers. Now we add one final trick to get the self reference, and construct a Godel number X that encodes the statement "Statement X is not provable in the formal proof system Y." We have managed to encode the nearest relation of the liar paradox as an arithmetical property of a particular number.
If the number X has this arithmetical property, then we can use our meta-understanding of what the arithmetical property means to conclude statement X is provable in Y, and use our meta-understanding of the encoding scheme to know that what we've proved is that statement X is unprovable in Y. This is inconsistent, and thus we know that formal proof system Y is inconsistent.
If the number X does not have this arithmetical property, then we use our meta-understanding of the arithmetical property to conclude X is unprovable. We use our meta-understanding of the encoding scheme to see that this is exactly what X says, and thus we meta-conclude that X is true, but Y is incomplete. There are true statements that it cannot prove.
In short, a logic powerful enough to talk about itself (such as Principia's arithmetic) is either incomplete or inconsistent. Because a logic powerful enough to talk about itself can express a version of the liar paradox, and the only way to avoid the paradox from destroying it is for the paradoxical statement to be unprovable.
The critical thing about all this is that the meta-system we use to interpret the numbers can be different from the system Y specified in the statement. If we try to use Y itself, and succeed, then the statement we've just proved is false and Y is inconsistent. If we use a different meta-system to do the interpretation, there is no such objection. "'Statement X is not provable in the formal proof system Y.' is provable in formal proof system Z." is perfectly fine.
So as a human, we can informally use human intuition as proof system Z, and know that the statement is true. Some people have tried to use this to demonstrate the superiority of humans over algorithms, because the human proof machine Z can always prove it, but formal system Y inevitably fails. This is not so.
We can see this in another classic logical conundrum: the paradox of the unexpected hanging. In this problem, the judge tells the condemned prisoner that he will be hanged at dawn during the following week but the execution will be a surprise to the prisoner. The prisoner reasons that it cannot happen on the last day, else it wouldn't be a surprise. He would know it was coming at sunrise the previous day. So it can't happen on the second to last day either, because he would know the sunrise before. And so on. And so it cannot happen on any day. The prisoner is safe! And thus it comes as a complete surprise to him when he is taken out at dawn and hung on Tuesday.
What we're doing here is making a statement like "The date of the hanging is not predictable by the prisoner." This has the same shape as our Godel sentence. X is the date of the hanging, 'provable' is replaced by 'predictable', and Y is the prisoner. Prisoner Y cannot predict the day of the hanging (his knowledge of the future is necessarily incomplete), because that creates an inconsistency. But the executioner can.
In general, we can exclude any category of prover just by including them in the statement to be proved. "This statement cannot be proved by humans." could, in theory, be proved (informally) by a machine. The statement "This statement cannot be proved by Nigel." can be proved by everyone except people called 'Nigel'. And so on. Humans are not excluded. They're just less bothered by the liar paradox rendering their reasoning system inconsistent.
Godel sentences can only be made precise if you specify what system is doing the proof, and so we always have an escape hatch in that we can always choose to prove it using a different formal system. We can thus prove that it is unprovable, because we are using two different meanings/definitions of 'proof'.