This is inspired by the MO question here.
Suppose I'm writing a math paper, with theorem and proofs, etc. At the end of writing, I want to design a graph of dependencies, that is, a graph containing every theorem, lemma, etc., and directed arrows for when one theorem relies on some other lemma, theorem, etc. in its proof. What would be a slick way of doing this?
I know the actual drawing of the graph will be hard, so I'm more interested in how to write this data to a file in an interesting way. Just redefining the proof
environment, for example, seems to work, but how to get the actual theorem numbers/names in the graph data? It seems one would have to actually redefine the ref command in a more subtle way, and I don't know how to do that.
It would be even cooler if you could control a few parameters, like maybe instead of looking "locally" at theorems, you could be more "global" and just look at chapter dependencies (and thus generate a Leitfaden), and maybe even more gradations in between. There could also be "threshold" parameters, so that one chapter has to reference another, say, 10 or more times before it becomes important enough to include in the graph data. You could even go crazy and include bibliography references too!
I don't know the appropriate tags for this, so feel free to change them.