How to write a 21st century proof
The author focuses on the problem of a proper method of writing informal proofs. The starting point is the observation that the style of writing mathematical proofs is still the same as in the 17th century. Informal proofs are often hard to follow (especially for beginners), and tend to hide errors, in particular when the proper scope of additional assumptions is not clearly stated. In the author's opinion, a good method of writing proofs, which was examined by him during the last twenty years, requires adding structure and naming. The former shows hierarchical construction of the proof and helps to avoid errors connected with scopes of assumptions. The latter makes easier the cross-reference in justification of proof steps. After a detailed analysis of an example proof taken from Spivak's textbook on analysis, the author describes TLA\(^+\), which is a formal language primary designed for specifying and reasoning about algorithms and computer systems, but which can be used also in ordinary mathematics. Moreover, in the appendix, one can find a completely formalised proof of the analysed example. The paper finishes with some comments of pedagogical nature and answers some objections formulated against structured proofs. The problem discussed by Lamport is important and his proposals quite interesting. But I found it surprising that he did not make any reference to other proposals of this kind. In particular, there is no reference (perhaps critical) to proposals based on principles of natural deduction, like, e.g., Mizar. A comparison with other approaches could be profitable.
- A scrapbook of inadmissible line complexes for the X-ray transform
- Formalising mathematics -- in praxis; a mathematician's first experiences with Isabelle/HOL and the why and how of getting started
- Structuring Mathematical Proofs
- scientific article; zbMATH DE number 3941513 (Why is no real title available?)
- scientific article; zbMATH DE number 1331926 (Why is no real title available?)
- A powerful method of non-proof
- How to Write a Proof
- NATURAL FORMALIZATION: DERIVING THE CANTOR-BERNSTEIN THEOREM IN ZF
- Plans and planning in mathematical proofs
- Programming and verifying a declarative first-order prover in Isabelle/HOL
- Strict linearizability and abstract atomicity
- Structured derivations: a unified proof style for teaching mathematics
- Squeezing streams and composition of self-stabilizing algorithms
- Proving a non-blocking algorithm for process renaming with TLA\textsuperscript{+}
- Proofs for a price: tomorrow's ultra-rigorous mathematical culture
- Certified first-order AC-unification and applications.
This page was built for publication: How to write a 21\(^{\text{st}}\) century proof
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q692371)
