[lakesare]

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?

[tunesmith]

Propositional, so no exists or foralls, but yes for ORs and NOTs. Acyclic only.

[lakesare]

Reminds me of characteristica universalis