Something to consider #4
Description
What should happen to a proof if one of its lemmas is deleted?
What happens to a proof if its theorem is deleted?
What happens to other theorems if one of their dependencies is deleted?
Also, I am still unclear of whether we display only theorems or theorem+proofs on the graph, because that makes a lot of difference to the dependency structure that we should implement in the models. Right now, the "any" and "all" dependency model works well for the (theorem+proof) display, because it is clear: a theorem depends on "any" of its proofs, and proofs depend on "all" of its lemmas. However, theorem-only visualization will have a problem showing a clear structure of partial-dependency and logical structure of the graph.