If there are two different proofs for one theorem, at some level are the two proofs the same, or can they be fundamentally different?

In other words, if you have two proofs of a theorem, can one show that the two proofs are expressing the same thing in different ways, and then remove the redundancies and generate a "shorter" proof?

-
It depends. For example the Prime Number Theorem has a Elementary proof as well as an Analytic proof and these two proofs are completely different. –  anonymous Jan 24 '11 at 16:02
can you explain what you mean by "completely different"? –  picakhu Jan 24 '11 at 16:03
There was a long discussion of this at mathoverflow.net/questions/3776/… . –  Qiaochu Yuan Jan 24 '11 at 16:31
@QY: Thanks, that was exactly what I was looking for. –  picakhu Jan 24 '11 at 16:39
–  Kaveh May 27 '11 at 7:57

They can be "completely different".

For example, some existence results have both indirect proofs and constructive proofs. There is often no way to interpret the "indirect proof" as "essentially the same" as the constructive proof.

Or you have the many different proofs of Quadratic Reciprocity. Gauss's first proof, in the Disquisitiones Arithmeticae, is very constructive; it is done by recursion, and for example it shows exactly how to transform a solution of $x^2\equiv p\pmod{q}$ into a solution of $x^2\equiv q\pmod{p}$ when $p$ and $q$ are not both congruent to $3$ modulo $4$; whereas his third proof was purely combinatorial, counting certain objects, and his sixth used Gauss sums, again an essentially different approach. Eisenstein used infinite products for his fifth proof, Kummer used quadratic forms, Zolotarev used permutations; Auslander and Tolimieri used the Fourier transform, Weil used theta functions. These are truly essentially different approaches, with no easy way to pare them down to the same thing (unless you "pare them down" to the statement of Quadratic Reciprocity itself).

-
Thanks, this is insightful, however, I was thinking about an algorithmic mathematical systems, where computers can generate proofs. If there are fundamentally different methods to prove something, doesn't that seem a bit weird? For example I was thinking was can a computer generate a Synthetic proof for a geometric question ? –  picakhu Jan 24 '11 at 16:22
@picakhu: I see not reason why "fundamentally different methods to prove something" would be "a bit weird". Unless your system happens to be rather poor, I would expect a lot of paths leading to the same points in the landscape. –  Arturo Magidin Jan 24 '11 at 16:28
I never thought about it that way! Thanks! –  picakhu Jan 24 '11 at 16:29