Existence of unknowable algorithms ?

Here is a pure existence proof of computability, where we show that a function is computable, not by exhibiting an explicit algorithm, but by providing a list of infinitely many algorithms, and proving that one of them computes the function; we just don't know which one.

(This answer is adapted from an answer I gave to Hans Stricker's question Non-constructive proofs of decidability?)

Let $f(n)=1$, if there are $n$ consecutive $7$s somewhere in the decimal expansion of $\pi$, and $f(n)=0$ otherwise. Is this a computable function?

Perhaps we might try naively to compute it like this: on input $n$, start to enumerate the digits of $\pi$, and look for $n$ consecutive $7$s. If found, then output $1$. But then we realize, of course: what if on a particular input, you have searched for 10 years, and still not found the instance? We don't seem justified in outputting $0$ quite yet, since perhaps we might still find the consecutive $1$s by searching a bit more.

Nevertheless, we can prove that the function is computable by a pure existence proof. Namely, either there are arbitrarily long strings of $7$s in $\pi$ or there is a longest string of $7$s of some length $N$. In the former case, the function $f$ is the constant $1$ function, which is definitely computable. In the latter case, $f$ is the function with value $1$ for all input $n\leq N$ and value $0$ for $n\gt N$, which for any fixed $N$ is also a computable function.

So we have proved that $f$ is computable in effect by providing an infinite list of programs and proving that one of them computes $f$, but we don't know which one exactly. Indeed, I believe it is an open question of number theory which case is the right one.

The question is a little vague but here is the answer to one possible interpretation of it. Let $R$ be a finite group presentation with finite generating set $X$, $u$ is a word in $X$. Suppose $G$ is generated by $X$, and finite, then we there is an algorithm to find out if $u=1$ in $X$ (the word problem in every finite group is decidable). But there is no way we can know if there exists a universal algorithm that given $R$ and $u$ tells if $u=1$ in every finite group generated by $X$ that satisfies $R$ (i.e. the uniform word problem in finite groups is undecidable, see Slobodskoĭ, A. M. Undecidability of the universal theory of finite groups. Algebra i Logika 20 (1981), no. 2, 207–230). In fact that situation is quite normal. Decidability of a mass problem means an algorithm to solve it exist, but often it is a pure existence statement.

If you are still not satisfied with any of the current answers, then I think the trouble is that you have not thought through clearly in your own mind what it means for it to be impossible to know some particular mathematical fact.

The first condition that you want to be satisfied is clear enough. You want it to be provably true that

There exists some Turing machine that solves My Favorite Problem.

Since Turing machines can be enumerated, this is equivalent to saying that we can prove that at least one of the statements in the following list is true.

Turing machine 1 solves My Favorite Problem.
Turing machine 2 solves My Favorite Problem.
Turing machine 3 solves My Favorite Problem.
Turing machine 4 solves My Favorite Problem.
$\vdots$

The second condition that you want to be satisfied is that not only do we currently not know any particular statement in this list to be true, but there should be some "intrinsic formal impossibility" preventing us from ever knowing it.

The trouble is that it's not clear what you mean by "an intrinsic formal impossibility." Suppose for example that Turing machine 314159 happens to solve My Favorite Problem. What's to stop someone from just baldly asserting, "I know that Turing machine 314159 solves My Favorite Problem"? Well, of course, being mathematicians, we object to people making such an assertion unless they can prove it. So probably you want your second condition to look something like this:

For every n such that Turing machine n solves My Favorite Problem, it is impossible to prove that Turing machine n solves My Favorite Problem.

Now the trouble with this statement as it stands is that it is not entirely formal, because we have not specified the axioms we are allowed to appeal to in our proof. In "ordinary mathematical life," we normally do not bother explicitly saying what axioms we allow. As trained mathematicians, we recognize a valid proof when we see it and that's good enough for ordinary mathematical work. However, once you start trying to make statements about the impossibility of proving something, you can't get away with this sloppiness any more. You have to specify some set of axioms. Otherwise, there's no way to stop someone from taking "Turing machine 314159 solves My Favorite Problem" as an axiom.

O.K., so we have to specify some set of axioms. So how about ZFC, everybody's favorite whipping boy? That's a reasonable choice. However, as Andreas Blass pointed out in the comments, once you fix a set of axioms, then something like Goldstern's answer works. Now of course Goldstern's answer seems like a cheat. We wouldn't want to be accused of cheating, would we? Of course not. So, let's choose some other set of axioms. Whoops, no good…any reasonable set of axioms will leave some statement undecided, and Goldstern's cheat slips in the door. Dang it, there must be some way to phrase the question so that no cheating answer is possible. Mustn't there?

I don't think there is. As soon as you find yourself dealing with one specific statement such as "Turing machine 314159 solves My Favorite Problem," there's no way to avoid this kind of "cheat" when it comes to saying what it means for it to be impossible to prove it.

The only other avenue I see for you to try is this: Instead of saying that for every n it is impossible to prove that Turing machine n solves My Favorite Problem, you could try asking this:

There is no algorithm that, given n, decides whether Turing machine n solves My Favorite Problem.

Ah! That sounds more like it! Or does it? The trouble is, you can choose just about any algorithmic problem you like and it will be undecidable whether Turing machine n solves it. This is Rice's theorem. So this isn't really what you want either, since it has nothing to do with the inscrutable structure of My Favorite Problem; it rather has to do with the inscrutability of Turing machines in general.

At the end of the day, I think you just have to accept the uncomfortable fact that there is no way to get an answer that is better than the ones that have been proposed already. There are problems for which we can currently prove that there is an algorithm but we don't know any algorithm yet, and we can prove that there is no general procedure for turning existence proofs of algorithms into constructive proofs, but if you try to push harder and ask for an explicit example of My Favorite Problem for which an algorithm is intrinsically unknowable, then you're inevitably going to run into the above difficulties.