How to write a 21\(^{\text{st}}\) century proof (Q692371)

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.