  As an example of empirical metamathematics, we present a detailed study of
the dependency structure of the 465 theorems in Euclid's Elements, finding
empirical signatures of concepts such as the power of a theorem. We apply
similar methods to a more exhaustive study of possible theorems in logic, as
well as to the analysis of dependency structures in projects to formalize
modern pure mathematics. We discuss the process of identifying both intrinsic
features of metamathematical space, and features of its exploration through the
historical progress of mathematics.
