[HN Gopher] Lean, Coq and other proof assistants: Visualising pr...
___________________________________________________________________
Lean, Coq and other proof assistants: Visualising proofs as trees
This is my overview of proof visualisation tools among all modern
proof assistants. If you're aware of any tools I might have
missed, please @ me in the comments. I aimed to cover every one I
could find.
Author : lakesare
Score : 55 points
Date : 2023-09-20 11:48 UTC (1 days ago)
(HTM) web link (lakesare.brick.do)
(TXT) w3m dump (lakesare.brick.do)
| tunesmith wrote:
| Well, I think a DAG would generally be better than a tree for
| visually representing a proof. Because a premise can support
| multiple lemmas.
|
| One site I've been working on uses graphs to generate arguments
| in that fashion:
|
| http://concludia.org/
| lakesare wrote:
| That's correct, in fact we would have a DAG if we displayed all
| possible arrows, but we conceal it to make the UI easier to
| interact with for the user. Hypotheses (green nodes) form many
| little trees, and goals (red trees) form a single tree. These
| must be trees, and not lattices, because that's just how Lean
| and Coq tactics work. However, tactics make use of hypotheses,
| and these can be displayed as arrows that connect hypotheses
| and goals, making it, in this sense, a DAG (here is an example,
| I moved the nodes a bit to make the arrows obvious
| https://github.com/Paper-
| Proof/paperproof/issues/9#issuecomm...). Concludia looks
| interesting, does it support first-order logic/ORs?
| Reubend wrote:
| Thanks for posting this. As a beginner, do I need to already know
| what "sequent-calculus-style trees" are for this to be useful?
|
| I didn't see any broad explanation of what the tree structure
| means here. I can see that disjunctions split a branch into 2
| branches, but I'm still pretty confused overall.
| lakesare wrote:
| It isn't necessary to know theory for these visualisations to
| be useful, both Traf and Paperproof (and sequence calculus
| trees!) should, ideally, just reflect what's already happening
| in your mental image while you're writing a Lean/Coq/on-paper
| mathematical proof. But I agree it warrants a
| tutorial/explanation, got to write it. I think it might be
| particularly unclear what's happening if you're just looking at
| the full tree of the already-proved-theorem. As we're writing
| the proof, hypothesis nodes (green, what we have) move down;
| and goal nodes (red, what we want to have) move up. So it kind
| of goes from both sides to the center, and you should read it
| "from both sides to the center", takes getting used to. Here is
| a video of what's happening in Paperproof as we're writing the
| proof e.g.: https://www.youtube.com/watch?v=0dVj4ITAF1o.
| cobbal wrote:
| Some searching found http://logitext.mit.edu/tutorial . It
| tries to explain sequent calculus with an interactive gui
| prover. Not sure how approachable it is... I've gotten too used
| to these things to know how to explain them properly.
| nathell wrote:
| 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....
| [deleted]
| mjfl wrote:
| What is it with proof assistant designers and terrible naming
| instincts? "Lean" as a name collides with all sorts of
| business/engineering productivity frameworks "Lean software
| development", "lean business management", "running a lean
| startup". And of course Coq is phallic both in English and the
| original French. It must be the case that the people that design
| these things live in a separate plane of existence where these
| things don't bother them.
| [deleted]
___________________________________________________________________
(page generated 2023-09-21 23:00 UTC)