Structured proofs

Techniques for writing structured, but informal, proofs. See related MathOverflow post about semi-formal proofs .

Literature

The community around the semantic representation of math has produced related work, e.g. MathDox , but seems to be stagnant.

Structured proofs, a line of work beginning in American Mathematical Monthly

  • Leron, 1983: Structuring mathematical proofs (doi)
  • Lamport, 1995: How to write a proof (doi, pdf)
  • Lamport, 2012: How to write a 21st century proof (doi, pdf)
    • Method for informal but structured proofs, inspired by TLA+
    • Blog posts at the Morning Paper (1 , 2 )
    • Lecture on TLA+ at 2018 Heidelberg Laureate Forum

Formal proof sketches

  • Wiedijk, 2004: Formal proof sketches (doi)
    • Sec. 6: Comparison with Lamport’s structured proofs
  • Barendregt & Wiedijk, 2005: The challenge of computer mathematics (doi)

Miscellaneous

  • Wells, 1995: Communicating mathematics: Useful ideas from computer science (doi, pdf)
    • Sec. 2.3: Definitions should be presented as specifications of external behavior, not set-theoretic constructions
    • Sec. 4.2.4: Tension between “syntactic” and “semantic” styles of mathematical writing
    • Sec. 4.4: Brief comment on Lamport’s structured proofs