I'm not sure where I fall on this. Sometimes I want to machine-validate
all of my proofs, and sometimes I feel it doesn't matter.
A couple arguments from the other direction:
- Reading and verifying each step of a proof is not necessarily enough
to understand the proof as a whole. So writing a proof without any
steps skipped doesn't alleviate the need to write a sketchy 'human'
proof to go along with it. Lamport's hierarchical proofs[1] are one
way to do both.
- It takes a long time to justify every step, especially if you want
to give references.
- Is it really necessary for us to be 100% certain that a proof is
correct? As a proof ages and more people read it without finding
errors, it becomes less and less likely that it's incorrect. For
most practical purposes, that's good enough.
A couple arguments from the other direction:
- Reading and verifying each step of a proof is not necessarily enough to understand the proof as a whole. So writing a proof without any steps skipped doesn't alleviate the need to write a sketchy 'human' proof to go along with it. Lamport's hierarchical proofs[1] are one way to do both.
- It takes a long time to justify every step, especially if you want to give references.
- Is it really necessary for us to be 100% certain that a proof is correct? As a proof ages and more people read it without finding errors, it becomes less and less likely that it's incorrect. For most practical purposes, that's good enough.
[1] https://research.microsoft.com/en-us/um/people/lamport/pubs/...