3 ms·
Why not make this rigorous and actually quantify how similar proofs are? I assume this could be done.
by VirusNewbie 2y ago
Why not make this rigorous and actually quantify how similar proofs are? I assume this could be done.
- colechristensen 2y agoYou 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. I strongly assume this would be hard.
- lanstin 2y agoSome 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.