In mathematics, one often makes (proves) statements on the basis of:
- Previously proven statements
I like to think of these dependencies as a directed graph, with edges from the accepted statements (from 1. or 2.) to the new statements.
Often times, the same statement can be proven from many (potentially infinite) different statements, so one can imagine, many variants of this graph. Similarly, there is a potentially infinite number of statements one can prove.
Still, has there even been an attempt to visualize, perhaps at a very high level, what a graph like this would look like across all branches of mathematics, say, assuming that one starts with ZFC and only considers the most well known theorems, and commonly taught statements and proofs?
Taking this a step further, would it make sense to consider a minimum spanning graph that cover well known theorems in mathematics? If so, how could one measure the goodness of a graph (or a proof) for a given set of statements? (can the "intuitive complexity of this graph" be captured?).
If I had to collapse this into a single question: Is this problem actively studied? Or is it something that draws little interest in mathematics?