Euclid's Proof that there are an infinite number of primes I'm trying to clarify my understanding of decidability of a language. The following question is totally made up by me so I hope it makes sense.   
Let $L = \{A: A \text{ is an algorithm that can prove "There are an infinite number of primes"}\}$
In light of the comments, what if I reformulate the question as:
Let $L = \{T: T \text{ is a theorem that has been proven true}\}$   
For example, "There are an infinite number of primes" is such a theorem.
Since Euclid proved that there are an infinite number of primes, does that mean L is decidable? If not, it must mean that Euclid's proof is not an algorithm. In that case, I'd like to understand why Euclid's proof is not an algorithm.
 A: As it stands, your question is hard to answer properly, because you don't formalize what kind of "algorithm" you have in mind, and how it proves "There's an infinite number of primes".
But there's a very general theorem in recursion theory, which basically says that any set of recursive functions (i.e. algorithms) which is defined in terms of the behaviour of it's member functions, rather than some syntactic property, is undecidable.
The reason is, roughtly, that you can always take an algorithm - even a trivial one that is easly shown to always terminate - and modify it so that before it terminates and returns its result, it attempts to solve some undecidable problem like a particular instance of the halting problem.
Thus, for all usual formalizations of "algorithm" and "proof", the answer to your question is no, $L$ is undecidable.
A: A language is decidable if there exists a Turing Machine that halts on all inputs and accepts on strings in the language. So your language is undecidable, as this is exactly the halting problem. If we have an algorithm, it will always halt, so a Turing Machine can accept it. However, a heuristic may not halt. So $L$ is recursively enumerable, but not decidable.
Now in terms of Euclid's proof, I would say this is not an algorithm. Given any finite set of primes (ie., suppose we have a finite  set of all the primes), an "algorithm" for Euclid's lemma will reject the set, inferring an additional prime. So what will it accept? There are infinite number of primes, but Turing Machines are restricted to finite input strings. So it's not computationally feasible to really deal with the set of all primes.
