lakesare
Joined 7 years ago
Karma
211
Submissions
35
Member since
Apr 26
https://github.com/lakesare
View on Hacker NewsRecent submissions
Comment · 1 year ago
Loving the sepia theme, and in general fells really pleasant to me (something I did lack in other writing software).
I think I will try it for my next project :)
Comment · 3 years 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.
Comment · 3 years ago
Reminds me of characteristica universalis
Comment · 3 years ago
I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.
Comment · 3 years 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#issuecomm...).
Concludia looks interesting, does it support first-order logic/ORs?
Comment · 3 years 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.