5 ms·

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

158 points by lakesare 3y ago

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.

SkyMarshal 3y ago
Cool idea. Here are about ~30 more that might be of interest. Not all are code proof assistants, just listing extras in case serendipity. https://pastebin.com/bYXWj7w6 https://pastebin.com/bYXWj7w6
NooneAtAll3 3y ago
> Metamath - Nothing? Does their default proof explorer[1] not count? [1] - https://us.metamath.org/mpeuni/mmtheorems.html https://us.metamath.org/mpeuni/mmtheorems.html
deleted 3y ago
[deleted]
Reubend 3y ago
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 3y ago
  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 https://www.youtube.com/watch?v=0dVj4ITAF1o.
- cobbal 3y ago
  Some searching found http://logitext.mit.edu/tutorial 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.
- colanderman 3y ago
  Sequent calculus trees [1] are straightforward. Essentially read them as: for each horizontal line, the judgment (assumptions ⊢ conclusion) below the line is valid if-and-only-if the judgments above the line are valid, by grace of the syntactic transformation rule named to the right of the line. These are stacked atop one another to form a tree, the leaves at the top (with nothing above the lines) being axioms of the system, the root at the bottom being the judgment whose proof is the tree. Sometimes the trees are upside down from this, for reasons I haven't been able to divine. Some logics also permit multiple (alternative) conclusions in a judgment, which is then properly called a sequent. Nearly the same notation is used for type judgements in type theory as well, with "assumptions ⊢ conclusion" being replaced by "environment ⊢ type assignments". [2] [1] https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK (The preceding section introduces the notation but uses the upside-down variant, for unclear reasons -- I've rarely seen it elsewhere.) [2] https://en.wikipedia.org/wiki/Type_theory#Technical_details https://en.wikipedia.org/wiki/Type_theory#Technical_details
nathell 3y ago
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.pdf https://lamport.azurewebsites.net/pubs/lamport-how-to-write....
- colanderman 3y ago
  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/Tutorial/Hierarchical_proofs.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T... [2] https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-reference https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-ref...
- zozbot234 3y ago
  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.)
- lakesare 3y ago
  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.
tunesmith 3y ago
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/ http://concludia.org/
- lakesare 3y ago
  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#issuecomment-1730438164 https://github.com/Paper-Proof/paperproof/issues/9#issuecomm...). Concludia looks interesting, does it support first-order logic/ORs?
  - tunesmith 3y ago
    Propositional, so no exists or foralls, but yes for ORs and NOTs. Acyclic only.
    - lakesare 3y ago
      Reminds me of characteristica universalis
mjfl 3y ago
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 3y ago
  [deleted]
- deleted 3y ago
  [deleted]
- lakesare 3y ago
  I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.
  - lupire 3y ago
    N for Natural numbers.
- hcta 3y ago
  you say that like it is a bad thing. Sign me up for the plane of existence without management frameworks please.
- nanolith 3y ago
  It's practically impossible to pick names that haven't been used for something else. I've taken to using the contraction of random amusing phrases when I want a unique name, but this isn't any better. Just fun (for me). Relevant example: my current toy proof engine and language is called lesc. There are lots of things called "lesc", but none of them to my knowledge stand for Less Elegant Space Cowboy.
- ahhfgshando6698 3y ago
  [dead]
throwaway2562 3y ago
Jonathon Gorard’s Abstract Proof Networks - in Mathematica - may be of interest https://community.wolfram.com/groups/-/m/t/1135271 https://community.wolfram.com/groups/-/m/t/1135271
isaacfrond 3y ago
A few years back I made a concerted effort to learn Isabelle, the HOL based theorem prover. Proofs read a bit like natural languages but are fully rigorous, moreover Isabelle has application in math as well as programming. What's not to like. What I found out was, that after diligently doing all the tutorials, and making all the exercises, there is still a huge gap between my skills and what is needed for real work. Note even that, you cannot even follow proofs of real theorems. Even with the reference manual in hand, trying to follow along word by word, there is a lot outright missing. From what I could gather, those that had successfully learned it did so at the hand of a master who explains the arcane incantations needed to get from proof state to proof state. I'd still love to learn a formal theorem proving language, any one really, and be able to do formal proofs, but i'm not sure how. Coq seems even more arcane than Hol/Isabelle. I'm not sure about Lean, but I'm skeptical about learning it without having an expert on call.
- jksk61 3y ago
  well, for lean I know there's a discord (with a fair amount of experts) and a fair share of resources nowadays. However, I did try 3 years ago and the jump between solving a simple algebra proof and contributing to Mathlib (or even understand something in it), is quite high. Coq is well designed/easy to understand but it is missing a core mathlib like Lean. Moreover, most proofs are designed to "compile" quickly and not to be human readable.
- practal 3y ago
  I hear you. I picked up Isabelle relatively easily, but I had the good fortune to be at one of the places where Isabelle is developed, and actually became later part of that group for my PhD. Still, even for me, dealing with various issues in Isabelle is frustrating (I will not even touch stuff like Coq or Lean, these are just insults on my mathematical senses). I know how this all can be made more accessible and natural and practical, and I am working on it. I, too, want to be using such a tool for real stuff. In particular, integrating LLMs with theorem provers is very promising, and I think the new logic I am developing is especially suited for it. You could argue, but well, a natural language interface is just the surface, and the complexity remains just under this surface. I would not argue against that in principle, but my new logic hopefully also takes care of a lot of unnecessary complexity and complications under the hood.
butokai 3y ago
For the Coq proof assistant, a recent approach to graphical proofs is Actema: https://www.actema.xyz/ https://www.actema.xyz/
NBJack 3y ago
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.

158 points by lakesare 3y ago

SkyMarshal 3y ago

Cool idea. Here are about ~30 more that might be of interest. Not all are code proof assistants, just listing extras in case serendipity. https://pastebin.com/bYXWj7w6 https://pastebin.com/bYXWj7w6

NooneAtAll3 3y ago

> Metamath - Nothing? Does their default proof explorer[1] not count? [1] - https://us.metamath.org/mpeuni/mmtheorems.html https://us.metamath.org/mpeuni/mmtheorems.html

deleted 3y ago

[deleted]

Reubend 3y ago

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 3y ago
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 https://www.youtube.com/watch?v=0dVj4ITAF1o.
cobbal 3y ago
Some searching found http://logitext.mit.edu/tutorial 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.
colanderman 3y ago
Sequent calculus trees [1] are straightforward. Essentially read them as: for each horizontal line, the judgment (assumptions ⊢ conclusion) below the line is valid if-and-only-if the judgments above the line are valid, by grace of the syntactic transformation rule named to the right of the line. These are stacked atop one another to form a tree, the leaves at the top (with nothing above the lines) being axioms of the system, the root at the bottom being the judgment whose proof is the tree. Sometimes the trees are upside down from this, for reasons I haven't been able to divine. Some logics also permit multiple (alternative) conclusions in a judgment, which is then properly called a sequent. Nearly the same notation is used for type judgements in type theory as well, with "assumptions ⊢ conclusion" being replaced by "environment ⊢ type assignments". [2] [1] https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK (The preceding section introduces the notation but uses the upside-down variant, for unclear reasons -- I've rarely seen it elsewhere.) [2] https://en.wikipedia.org/wiki/Type_theory#Technical_details https://en.wikipedia.org/wiki/Type_theory#Technical_details

nathell 3y ago

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.pdf https://lamport.azurewebsites.net/pubs/lamport-how-to-write....

colanderman 3y ago
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/Tutorial/Hierarchical_proofs.html https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T... [2] https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-reference https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-ref...
zozbot234 3y ago
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.)
lakesare 3y ago
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.

tunesmith 3y ago

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/ http://concludia.org/

lakesare 3y ago
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#issuecomment-1730438164 https://github.com/Paper-Proof/paperproof/issues/9#issuecomm...). Concludia looks interesting, does it support first-order logic/ORs?
- tunesmith 3y ago
  Propositional, so no exists or foralls, but yes for ORs and NOTs. Acyclic only.
  - lakesare 3y ago
    Reminds me of characteristica universalis

mjfl 3y ago

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 3y ago
[deleted]
deleted 3y ago
[deleted]
lakesare 3y ago
I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.
- lupire 3y ago
  N for Natural numbers.
hcta 3y ago
you say that like it is a bad thing. Sign me up for the plane of existence without management frameworks please.
nanolith 3y ago
It's practically impossible to pick names that haven't been used for something else. I've taken to using the contraction of random amusing phrases when I want a unique name, but this isn't any better. Just fun (for me). Relevant example: my current toy proof engine and language is called lesc. There are lots of things called "lesc", but none of them to my knowledge stand for Less Elegant Space Cowboy.
ahhfgshando6698 3y ago
[dead]

throwaway2562 3y ago

Jonathon Gorard’s Abstract Proof Networks - in Mathematica - may be of interest https://community.wolfram.com/groups/-/m/t/1135271 https://community.wolfram.com/groups/-/m/t/1135271

isaacfrond 3y ago

A few years back I made a concerted effort to learn Isabelle, the HOL based theorem prover. Proofs read a bit like natural languages but are fully rigorous, moreover Isabelle has application in math as well as programming. What's not to like. What I found out was, that after diligently doing all the tutorials, and making all the exercises, there is still a huge gap between my skills and what is needed for real work. Note even that, you cannot even follow proofs of real theorems. Even with the reference manual in hand, trying to follow along word by word, there is a lot outright missing. From what I could gather, those that had successfully learned it did so at the hand of a master who explains the arcane incantations needed to get from proof state to proof state. I'd still love to learn a formal theorem proving language, any one really, and be able to do formal proofs, but i'm not sure how. Coq seems even more arcane than Hol/Isabelle. I'm not sure about Lean, but I'm skeptical about learning it without having an expert on call.

jksk61 3y ago
well, for lean I know there's a discord (with a fair amount of experts) and a fair share of resources nowadays. However, I did try 3 years ago and the jump between solving a simple algebra proof and contributing to Mathlib (or even understand something in it), is quite high. Coq is well designed/easy to understand but it is missing a core mathlib like Lean. Moreover, most proofs are designed to "compile" quickly and not to be human readable.
practal 3y ago
I hear you. I picked up Isabelle relatively easily, but I had the good fortune to be at one of the places where Isabelle is developed, and actually became later part of that group for my PhD. Still, even for me, dealing with various issues in Isabelle is frustrating (I will not even touch stuff like Coq or Lean, these are just insults on my mathematical senses). I know how this all can be made more accessible and natural and practical, and I am working on it. I, too, want to be using such a tool for real stuff. In particular, integrating LLMs with theorem provers is very promising, and I think the new logic I am developing is especially suited for it. You could argue, but well, a natural language interface is just the surface, and the complexity remains just under this surface. I would not argue against that in principle, but my new logic hopefully also takes care of a lot of unnecessary complexity and complications under the hood.

butokai 3y ago

For the Coq proof assistant, a recent approach to graphical proofs is Actema: https://www.actema.xyz/ https://www.actema.xyz/

NBJack 3y ago

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.