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.
I strongly assume this would be hard.