This of course is a deep question in the philosophy of mathematics. The program mentioned by Tom Leinster is certainly a very interesting contribution to this, but if it proceeds at a purely mathematical level then at most it can define an equivalence relation on the class of proofs. There's still a further question whether this equivalence relation really is "the right one" to capture the notion of "same" or "different" proofs.

Also, note that there's an open question as to whether mathematical proofs really are the sort of thing studied by proof theorists. Certainly the sort of thing that is published in a math journal is not the sort of thing that is studied by proof theorists. To cite the most obvious differences, the former have words of English in them (or French or Japanese or Russian or some other language) while the latter don't. But for more significant differences, note that the former also cite well-known results from the literature, and skip steps that are sufficiently obvious to the reader, while the latter don't.

You can avoid this problem by assuming that published proofs are converted into formal proofs by means of spelling out all the steps in the proof of the well-known theorem, or the obvious fact. But this might not preserve the notion of "same proof".

For instance, consider a theorem that in some sense only has one proof, which happens to rely essentially on quadratic reciprocity. Do we really want to say that this theorem actually has just as many distinct proofs as quadratic reciprocity does?

There are lots of interesting questions here about the relation of proof theory to actual proofs, and what light it can shed on this intuitive notion of sameness of proof. And of course, there is probably also light to be shed in the other direction too, as our technical mathematical results in proof theory and category theory absorb results from the intuitive ideas we have about proof sameness.