Comment by tunesmith

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/