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?