The gist of the article is of course correct, but it uses some terminology wrong. "Recursively enumerable" and "decidable" aren't applicable to instances of ind

The gist of the article is of course correct, but it uses some terminology wrong. "Recursively enumerable" and "decidable" aren't applicable to instances of individual programs. In fact, every single instance of a problem is "decidable" because either the program that always returns true or the one that always returns false solves it (we don't necessarily know which one, but that isn't required). And in any case, for the Goldbach conjecture, the set of numbers that satisfy it is decidable - the function sum_of_two_primes is such a decision procedure. What's undecidable is the set of valid conclusions (from some axioms) in first-order logic (in short, "FOL is undecidable"). So there is no algorithm that can tell us whether a given mathematical statement (including Goldbach's conjecture) is "true" (i.e. follows from the axioms of arithmetic, or ZFC, or something). FOL is recursively enumerable, since we can just generate all possible proofs. Similarly, the set of halting programs isn't decidable, but it is recursively enumerable (every halting program halts at some time t, now enumerate all pairs (program, t) via a diagonal argument and check if program halts within t steps).