Proof maintenance

Leslie Lamport coined the phrase “proof maintenance” to describe the process of producing variations of a proof over time.

It’s well known that software needs to be maintained; most of the work on a program occurs after it is “finished.” Proof maintenance is common as well, but it is usually very informal.

Proofs of any significant length have an implicit hierarchical structure of sub-proofs and sub-sub-proofs etc. Sub-proofs may be labeled as lemmas, but that’s usually the extent of the organization. Also, the requirements of a lemma may not be precisely stated, and the propositions used to prove the lemma may not be explicitly referenced. Lamport recommends making the hierarchical structure more formal and fine-grained, extending the sub-divisions of the proof down to propositions that take only two or three lines to prove. See his paper How to write a 21st century proof.

When proofs have this structure, you can see which parts of a proof need to be modified in order to produce a proof of a new related theorem. Software could help you identify these parts, just as software tools can show you the impact of changing one part of a large program.

Related: Formal validation methods

Leave a Reply

Your email address will not be published.