"Family Tree" of Theorems Is anyone aware of any attempt to describe the dependencies of theorems (perhaps in mathematics generally, perhaps in some limited areas) in the form of a "family tree"?  That is, each node on the tree might correspond to a theorem, and branches would indicate dependencies between theorems?  I realize that this would not constitute an actual tree -- as there can exist loops -- but this sort of meta-description of theorems might provide some insight not available in other manners.  
[Added:] Except in some very formalized proof systems, making the  notion of dependency precise is probably difficult, if not impossible.  But colloquially, people will often make statements such as "Theorem A is used / can be used to prove Theorem B".  I'm sure everyone here can think of many such statements to which few will object.  For those cases, it might be very nice to have some accessible database with this information.  Not only might the data in this "graph" be practically useful (e.g., I want to write an expository paper about five interesting consequences of the Borsuk-Ulam theorem), but perhaps even some "meta-data" might provide valuable insight.  Just a thought.
 A: Concerning (parts of) algebraic geometry, the Stacks Project offers so-called dependency graphs.
A: Formal vs self-organised knowledge systems: a network approach
A.P. Masucci, Physica A 390 (2011) 4652-4659 (arXiv:1105.1058)

In this work we consider the topological analysis of symbolic formal systems in the framework of network theory. In particular we analyse the network extracted by Principia Mathematica of B. Russell and A.N. Whitehead, where the vertices are the statements and two statements are connected with a directed link if one statement is used to demonstrate the other one. We compare the obtained network with other directed acyclic graphs, such as a scientific citation network and a stochastic model. We also introduce a novel topological ordering for directed acyclic graphs and we discuss its properties in respect to the classical one. The main result is the observation that formal systems of knowledge topologically behave similarly to self-organised systems.

This paper looks at how logical statements such as theorems are organized in specific expository works (like the Principia). As others have noted in the comments, outside such organized works, the dependencies can be ambiguous as theorems can have alternate proofs. Moreover, the order of deriving theorems is not canonical so that if all proof paths were included, cycles will have formed. The Principia is as good as any work to start with, but I would really love to see a similar analysis on Bourbaki and on Euclid's Elements.

Figure from the paper: distribution of in and out degrees in the Principia DAG, in the DAG of citations, and in a stochastic generative model.
A: There are fairly recent dependency graphs relating to Euclid's Book 1, Elements, in the literature.
See A Boxer's paper in Bridges Art/Math 2015
Also see M. Schiefsky (Harvard Classics) and Boman (Penn State Math) and Nyugen (Berkeley) for overviews and graphs.
The most interesting is that of Jesse Atkinson, Bridges Art/Math 2016, that shows a 3-D in-tree dependency graph of Euclid's proof of the Pythagorean Theorem (1.47) embedded in a discussion about the overall role of 1.45 and 1.47 in that book.  It is an elegant "little" paper, by an undergraduate math student, to say the least.
A: The idea of "dependencies" is somewhat ill-defined. The Reverse Mathematics Program has one way of defining dependencies by comparing the theorems over a very weak base theory called RCA0. To see nice diagrams stemming from this program, check out the Reverse Mathematics Zoo!
