Gödel proved that there are true sentences that cannot be proved.

Suppose I told you that the Goldbach conjecture is one of those. (The Goldbach conjecture supposes that every even integer number can be expressed as the sum of two odd primes.)

Is that logically possible? (And, no, I haven't proved it!)

Federico:

You said, "suppose I programmed a computer to successively test every even number". That can't be done--there's an infinity of them. Further more, you will eventually come to a number too large for the computer to store--no matter how big the computer is. Consider the even number that has more digits than the number of atoms in the universe. No computer will ever be able to hold such a number.

You then said if it never found a counter example, that would prove the conjecture. But as long as it doesn't find a counter example it keeps running. So the proof you're talking about never happens.

You may be right that we "cannot prove that it cannot be proved." But that isn't what Godel asserts. He only asserted that in any formal system of number theory, there exist statements that are true, but cannot be proved...i.e., derived from the axioms.

So, until someone finds a proof or counterexample to the Goldback conjecture, we have to admit that it's POSSIBLE that it's one of these Godel statements that are true but have no proof.