Live data from Hacker News

Lean, Coq and other proof assistants: Visualising proofs as trees

lakesare.brick.do

31–33 of 33 posts

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#31
post #4

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....

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.)

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#32
If there's one thing I never felt I properly learned in comp sci, it's proofs. I sucked at them, and I'm grateful I don't need them as part of my job.

That said, are there any good resources that can teach me how to reason through proofs better? Preferably for someone who has a weak mathmatical background? Aside from the Pidgeon Hole theorem, they never clicked with me.

Re: Lean, Coq and other proof assistants: Visualising proofs as trees

#33
post #4

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....

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.

Post reply on HN