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....
Lean, Coq and other proof assistants: Visualising proofs as trees
31–33 of 33 posts
Re: Lean, Coq and other proof assistants: Visualising proofs as trees
#32That 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
#33Reminds 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....
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.