>I agree with pkoird's point that philosophically, two correct proofs of the same theorem should be considered "the same". Any theorem is ultimately a property of the natural numbers themselves along with the various paths that lead there from the axioms (since all proofs are essentially a finite sequence of Gödel numbers).
As with a lot of philosophy, the argument turns out to actually be much more about defining terms being used than the objects those terms are referring to. I mean when you are making an argument about "x is the same as y because..." your philosophical argument is actually about what should be meant by the same instead of any particular properties of x or y.
The article seems to be digging at the existence of a few categories of proofs
* proofs that are trivially transformed into one another
* proofs that use substantially similar arguments that don't necessary have a direct transformation
* proofs that arrive at the same destination through a much different path that have no obvious transformation to another proof
So the question is: how easy does it have to be to transform one proof to another in order for them to be considered "the same"?
One extreme is "the slightest change in wording makes a proof unique"
The other extreme is "any two proofs of the same concept are by definition the same proof"
I would argue that neither extreme is particularly useful, because both are just obvious. One means "these are different sheets of paper" and the other means "these are both proofs of X", neither of which are interesting statements.
What is an interesting statement is commentary on the path made to a proof and the differences in paths to proving a statement. Both in the ability to transform one into another easily to show similarity, and in the difficulty to transform one into another to show divergence.
You would need a rigorous way to encode proofs likely akin to Gödel numbering or at least something related to automated theorem proving and then add on transformation mechanisms and then rigorously prove that all proofs have transforms from one to the other.
Some sort of Hamming distance in Lean proofs perhaps? Seems unlikely to capture the difference in what a person would say are different proofs tho. And even when people say a proof is different from another one there is usually some notion of "according to our current understanding" with the idea that some further result could show that the apparently unrelated results are aspects of some deeper unity.
As with a lot of philosophy, the argument turns out to actually be much more about defining terms being used than the objects those terms are referring to. I mean when you are making an argument about "x is the same as y because..." your philosophical argument is actually about what should be meant by the same instead of any particular properties of x or y.
The article seems to be digging at the existence of a few categories of proofs
* proofs that are trivially transformed into one another
* proofs that use substantially similar arguments that don't necessary have a direct transformation
* proofs that arrive at the same destination through a much different path that have no obvious transformation to another proof
So the question is: how easy does it have to be to transform one proof to another in order for them to be considered "the same"?
One extreme is "the slightest change in wording makes a proof unique"
The other extreme is "any two proofs of the same concept are by definition the same proof"
I would argue that neither extreme is particularly useful, because both are just obvious. One means "these are different sheets of paper" and the other means "these are both proofs of X", neither of which are interesting statements.
What is an interesting statement is commentary on the path made to a proof and the differences in paths to proving a statement. Both in the ability to transform one into another easily to show similarity, and in the difficulty to transform one into another to show divergence.