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 :)
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.
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?
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.
A blog post where I catalog all Lean [proof assistant] books that exist in nature, share my opinion on them, and suggest learning paths for Lean novices.
It does violate the perfect "Cartesian coordinates" normalization I described earlier, however I consider this is a permissible step up over the full normalization, because, while cutting down repetition (entirely), it still suggests a zero-ambiguity way to read off the values from the header cells.
This certainly looks prettier than the initially shown full-fledged table structure, however I'm having more trouble reading it - it makes me slightly uncertain what text belongs to what row, and whether I properly track the row lines with my eyesight.
