When are two proofs "the same"?
Often, we find different proofs for certain theorems that, on the surface, seem to be very different but actually use the same fundamental ideas. For example, the topological proof of the infinitude of primes is quite different than the standard one, but the arguments are essentially the same, just using different vocabulary.
So, my question is the following:
Is there a rigorous notion of "proof isomorphism"?
Solution 1:
The question of proof equivalence is quite an old one! In fact, David Hilbert considered adding it (or a similar one) to his celebrated list of open problems, but finally decided to leave it out, so it is sometimes referred to as Hilbert's 24th problem.
There is a rather well-established field investigating proof equivalence, though definitely no clear answer to either your or Hilbert's question (and it is likely that this is quite out of reach). However, here are some various notions of proof equivalence of increasing strength.
Equality w.r.t. variable re-naming (also called $\alpha$-renaming). This is much too fine: clearly there are proofs that are "morally" the same, but that differ by more than variable re-namings.
Equality w.r.t. definition unfolding. This doesn't solve all of the above problems, but it's clear that if one proof involves a compact definition and the other does not, they should be seen to be the same.
Equality w.r.t. cut elimination. This one is much more interesting! For two proofs $\Delta$, $\Phi$, we say that $\Delta\simeq_{\mathrm{cut}}\Phi$ if the two proofs are the same (modulo variable re-naming) after having eliminated all cuts. Now a lot of rather different proofs become quite similar, e.g. proofs in calculus involving abstract "open/closed" terminology can be reduced to simple proofs involving $\epsilon$-$\delta$ notation. This still isn't satisfactory since e.g., some hypotheses can be used in different orders, or some useless steps still remain. It's also not clear that this is not too coarse, since sometimes the use of crucial lemmas makes a proof much simpler, and cut-elimination makes all intermediate lemmas "disappear".
Equality w.r.t. cut elimination with commutative cuts. See, for example these really nice slides by Clement Houtmann. This might get closer to the "right" notion, though as you can see things start to get a bit subjective at this point. What does it mean to "use the same idea"?
As Bruno mentioned, there is a deep connection between proofs of propositions and certain programs in particular programing languages, so one may re-formulate the question as
When are two programs the same?
with very fruitful results. The conclusion should be that this is a very active area of research in proof theory, with connections to computer science and categorical logic.
Solution 2:
This proof irrelevance is one of the problems of classic foundations.
In Type Theory, however, we represent mathematical statements as types, which enables us to treat proofs as mathematical objects. This is because of a well-known isomorphism between types and propositions a.k.a. Curry-Howard Correspondence, which roughly says that to find a proof of a statement A is to find a inhabitant of this type: $$a:A$$ Which, in the point of view of logic, can be read 'a is a proof of the proposition A'.
In this sense, to prove a proposition is to construct an inhabitant of a type, which means that every mathematical proof can be seen as an algorithm. This is related with "constructive" (intuitionistic) conception of logic where (i) to prove a statement of the form "A and B" is to find a proof of A and a proof of B, (i) to prove that A implies B is to find a function that converts a proof of A into a proof of B (iii) every prove that something exists carries with it enough information to exhibit such object and so on. Hence equality of elements of a type (proofs) is treated intensionally.
Now Homotopy Type Theory thinks of types as "homotopical spaces", interpreting, as stated in the comments, the relation of identity $a=b$ between elements (proofs) of the same type (proposition) $a,b: A$ as homotopical equivalence, understood as a path from the point $a$ to the point $b$ in the space $A$. The HoTT book is available for free in the project website.