Here by «algorithm» I mean a (halting) Turing machine with finite alphabet and memory.

Is it possible to obtain by purely existential (*i.e.* non-constructive) means the existence of an algorithm performing some required task, while beeing unable to explicit it (*i.e.* write it down or describe it constructively) ?

I hope the question is neither too vague nor too ill-posed, as I'm not so acquainted with these concepts! Thank you for any insight on the matter, feel free to retag or plainly close this naïve question if necessary.

**Edit:** in view of the answers given so far I think I can better explain what I meant originally. My question is more along the lines of

*Is there a task for which an algorithm is known to exist while at the same time it is not possible to recognize the said algorithm?*

By this I mean that our innability to perform the recognition is not a consequence of our current lack of actual knowledge, but of an intrinsec formal impossibility to do so. In other word working out that any algorithm outputs what is expected by the task is undecidable by inspection of its content.

**(Final) edit:** I thank everybody who took the pain to answer my rookie's question... I would like to formulate some comments regarding the (legitimate) objections that has been raised. First we may assume that the formal system is ZFC, in order to fix ideas.
My question was not about "mass problems" (although the examples presented below really are interesting), I was rather asking about a specific task, so it relates more to undecidability problems, as was pointed out by Mark Sapir.

Actually MyFavouriteProblem concerns effective computability of holomorphic dynamical systems satisfying MyFavoriteProperty, which were known to exists by some "abstract" argument and for which I gave a more "constructive" proof. It is doubtlessly a practical improvement (my PC can do the computing), but I wanted to know if from a theoretical point of view some progress really has been made (actually to settle a friendly argument with a colleague of mine). So the starting point to this question lies in algorithms performing computations with arbitrary floating-point precision on complex numbers, understood as Taylor coefficients of power series (needs some infinite memory here, I'm afraid, but I don't think it really matters).

Regarding Joel's answer: this argument would be a striking satisfactory answer if it is proved that knowing the value of $N$ is indecidable in ZFC. Maybe one can work out an example where $\pi$ is replaced by some other real number.

Regarding Goldstern's answer (and subsequent comment/answers): I don't so much think that the argument is a cheat than it does not answer my edited question (edit made after the initial answer). My point is the following. Either some open question $Q$ is decidable in ZFC, in which case we all agree that the program "Yes" or the program "No" answers $Q$, but by inspection of the programs we can decide which one performs the required task

*once we know which answer is a fact, which is not a formal issue anymore*. Either $Q$ is indecidable in ZFC and we cannot prove, in ZFC, the existence of an algorithm answering it (though I'm not sure of this part of my argument). Now if we attach $Q$ to our axioms set then we are back to the previous case, were answering $Q$ has become explicitely tautological. So I believe Goldstern's example does not meet the requirement of my question.Timothy's answer is great since it offers a very nice comprehensive summary of the issue as I perceive it. If the unofficial answer to my question is that pessimistic statement, then let it be. The sloppy mathematician in me is perfectly happy with matters as they are ;)

To conclude, I think I should accept Peter Shor's answer, since he gives an example which, as I understand it, answers my query. I'll do that in a little while.

8more comments