A fellow mathematician and myself are looking to begin a project to make life easier for working mathematicians by specifying a syntax for mathematical object definition and proof with the goals of
- Making the syntax easily translatable from written proofs using standard linguistic proof atoms “therefore it follows that” etc
*Linking chains of proofs by dependency
If anyone is interested in such a project we’d love additional contributors.
Is it related to writing hierarchically structured proofs?
That proof method also appears to be (or at least very similar to) the method Velleman describes in How to Prove It.
What’s interesting is (from a brief skim) Lamport in the second paper describes how mathematicians, famous for creating precisely-defined syntax and structure to describe mathematical objects, somehow recoil at the idea of a precisely-defined structural approach to proofs themselves and prefer the “more beautiful” but less precise narrative form that glosses over many of the details.
As someone who was interested in more abstract math concepts but had great difficulty learning any of the concepts as a largely self-taught student, can I humbly recommend that any such endeavor also learn and draw from the late Charles Wells’ Handbook of Mathematical Discourse as well as his broader site https://abstractmath.org (maintained by his family now).
I (and many others) learned a great deal by reviewing the contents of both. He specifically designed these to act as a bridge for those interested students to “level up” to where they could understand more abstract concepts, based on his experience teaching a wide variety of students at different levels.
An example is the You Don’t Know Shriek from the Handbook:
This is the indignant shriek that begins, “You mean you don’t know … !?” (Or “never heard of … ”) This is often directed at young college students who may be very bright but who simply have not lived long enough to pick up all the information a middle aged college professor has. I remember emitting this shriek when I discovered as a young teacher that about half my freshman calculus students didn’t know what a lathe is. In my fifties the shriek was emitted at me when two of my colleagues discovered that I had never heard of the prestigious private liberal arts college they sent their offspring to.
This phenomenon should be distinguished from the annoyance expressed at someone who isn’t paying attention to what is happening or to what someone is saying.
The name is mine. However, this phenomenon needs a more insulting name guaranteed to embarrass anyone who thinks of using it.