Undecidable conjectures Suppose we work with a conjecture saying that something is true for any natural $n$. For each $n$ there exists an algorithm of finite length allowing one to decide whether it is true or false for this $n$, and suppose that we even have an explicit formula how the length depends on $n$. It is proved that the conjecture is true for all numbers until, say, $10^{1000}$; no counterexample is found. Is it possible that this conjecture is undecidable? 
As far as I understand, the answer is yes, but I do not understand the following. If the conjecture is false, then we can take the corresponding $n$ and hence we get a finite proof of that fact. If it is undecidable, than we may add the axiom that it is false, and then we seem to arrive at a contradiction with my preceding phrase. Could anyone explain what is wrong?
 A: We will show where your intuitive argument breaks down. Call the conjecture $\varphi$, and suppose that $\varphi$ is undecidable. Then, as you observed, under your very strong assumptions, $\varphi$ is true in the natural numbers, but not provable. 
Not provable in what theory? By undecidable we always mean undecidable in a particular theory. Say that theory is PA, first-order Peano Arithmetic. But for the rest of this post, PA could be replaced by any strong enough theory that has the natural numbers as a model.
Let us add to PA  the axiom $\lnot\varphi$ as you specified. Then the theory $T$ with axioms the axioms of Peano Arithmetic, together with $\lnot\varphi$, is  consistent, and therefore has a model $M$.  In $M$, the conjecture $\varphi$ is false. 
This model $M$ is not (isomorphic to) $\mathbb{N}$, since $\varphi$ is true in $\mathbb{N}$.  The object $\omega\in M$ that "witnesses" the falsity of $\varphi$ in $M$ is therefore not a natural number. Your algorithm will not be applicable to $\omega$, which is, in the informal sense, greater than $1$, $1+1$, $1+1+1$, and so on. (We can without loss of generality assume that $\mathbb{N}\subset M$). Informally, under your assumptions, any $\omega$ that witnesses the falsity of $\varphi$ in $M$ must be an "infinite" integer.  
If a certain argument breaks down, it is still possible that the result one is after is true!  However, we can find explicit examples of sentences $\varphi$ of the type you described that turn out to be undecidable in PA.  
In particular, one can construct an  explicit Diophantine equation $E$ (in $k$ variables, where $k$ is not very large, last I heard about $20$) which has no solutions in $\mathbb{N}$, but such that this fact is not provable in PA.  Let $\varphi$ be the assertion that this Diophantine equation has no solutions. For any specific $k$-tuple $(a_1,a_2, \dots, a_k)$ of natural numbers, the fact that $(a_1,a_2,\dots,a_k)$  is not a solution of $E$ is easily checkable, by a computation of predictable length. By suitably encoding  the $k$-tuples of natural numbers, we can make sure that $\varphi$ satisfies your conditions. 
A: Goldbach's conjecture (which states that if $n\ge4$ is even then it is a sum of two primes) is of this type. If it's false, then there's a counterexample, and so a proof that it's false; hence, if it's undecidable (within some particular axiom system), then it's true. 
The twin prime conjecture (that there are infinitely many primes $p$ such that $p+2$ is also prime) is a different kettle of fish. The argument above does not apply, so it could be undecidable in a stronger sense. 
A: Assume you are working on the conjecture of consistency of PA (denote it $con(PA)$) in PA itself. $con(PA)$ essentially says for each $n$, it is not the case that $n$ is the Godel number of a proof of a contradiction - i.e. $con(PA)$ denotes the formula $\forall x \lnot Prov(x, 0 = 1)$. So $con(PA)$ is a type of conjecture you are looking at. 
We know that for each natural number $n$, ${\rm PA} \vdash \lnot Prov(n, 0 = 1)$. The universal quantification (i.e. $con(PA)$) on the other hand, is not provable in PA. If you add $\lnot con(PA)$ to PA, then you end up with a theory that is consistent, but not $\omega$-consistent. The later means that the theory proves $\exists x p(x)$ and
$\lnot p(0), \lnot p(1), ...$ for some $p$.
