Remix.run Logo
amanaplanacanal 2 days ago

Do you have the weekend free? Perhaps you can take this new proof and show us how it is done.

DoctorOetker 3 hours ago | parent [-]

If one is given an incomplete proof (i.e. where not each step is justified in terms of theorems completely justified before it) there is an amount of bruteforce entropy involved for guessing which intermediate steps weren't jotted down. Of course it takes 20x or more effort if the prover refused to write down certain steps. It even occurs that when pointed out, it takes the original "prover" a lot of time to find a proof for a gap, hence it wasn't originally proven.

If I find my own proofs, or if the proof of someone else is clearly written, formalization is not hard at all.

Let us assume for the sake of this discussion that Wiles' latest proof for FLT is in fact complete, while his earlier proof wasn't. It took Wiles and his helper more than a weekend to close the gap. Imagine no one had challenged the proof or pointed out this gap. Anyone tasked with formalizing it would face the challenge of trying to figure out which result (incorrectly presumed to be already known) was used in a certain step. The formalizer is in fact finishing an unfinished proof.

After succeeding in closing this gap, who else was willing to point at the next gap? There is always some sense of prestige lost when pointing at a "gap" and then observing the original prover(s) close that gap, in a sense they saw how to prove it while the challenger did not. This dynamic is unhealthy. To claim a proof we should expect a complete proof, the burden of proof should lay on the proving claimant not on the verifier.