Hacker News Reader

Comment by nathell | Hacker News Reader

Reminds me of Leslie Lamport’s „How to Write a Proof” [1]. I wonder whether there exist tools that aid in manually writing visualisable proofs?

https://lamport.azurewebsites.net/pubs/lamport-how-to-write....

View on HN

Structured proofs as advocated for by Leslie Lamport are more reminiscent of natural deduction. One obvious difference with sequent calculus is that natural deduction only admits of a single goal for each proof step (though with multiple antecedents or conditions), whereas sequent calculus generalizes this to multiple goals which are understood disjunctively i.e. "at least one" has to be true. (The latter works well with the inherent duality of some types of logic, such as ordinary classical logic or linear logic. It doesn't seem to come up all that much when doing math practically, especially in areas close to CS where "direct" proofs are generally preferred.)

Thanks for the link. I've been reading Leslie Lamport's TLA works this year coincidentally, but never stumbled upon this one. His structured proofs would turn into a paperproof-style tree if he turned his 3.1.1.1. numbers into a tree, it's pretty close to paperproof conceptually.

I don't know of any software that allows for manual writing of such proofs yet, I'm drawing proof trees on paper at the moment. I would like paperproof to allow for this eventually. We want to enable ml-generation of tactics with ReProver, which will require the interface for the manual creation of goals and hypotheses. Hopefully after that it will be more clear what fully-manually-written proof interface could look like.

Interesting, the notation used in that paper presages the notation used by TLA⁺² [1]. I actually have written up an exposition of TLA⁺² proof steps using sequent calculus notation [2] with the intention of writing a proof visualizer for it.

[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...

[2] https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-ref...

Reply on news.ycombinator.com