A graph of all of mathematics

Question

In mathematics, one often makes (proves) statements on the basis of:

1. Previously proven statements
2. Axioms

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?

Answer 1

"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 [emphasis added] branches of mathematics, say, assuming that one starts with ZFC and only considers the most well known theorems, and commonly taught statements and proofs?"

This is impossible, even if one wanted to visualize what such a graph looks like just in the case of propositional calculus, if we allow derived rules of inference (and don't mathematicians commonly make use of derived rules of inference?).

For instance, let's say we considered a propositional calculus with just 1: CpCqp and 2: CCpCqrCCpqCpr with detachment as the sole primitive rule of inference (I use Polish notation). Now all proofs can get represented by a proof tree like the following:

      X   Y
       \ /
        Z

where some substitution instance of X and Y have gotten used to infer Z by detachment, where X and Y already belonged to our theorem list. So all permissible proofs in this propositional calculus can get represented by such trees which only use the rule of detachment.

However, due to the rule of detachment there exists a powerful meta-theorem which says that

"if $\gamma$ $\vdash$ C$\alpha$$\beta$, then {$\gamma$, $\alpha$} $\vdash$ $\beta$".

Now from that meta-theorem and having CCpCqrCCpqCpr as a axiom, we have as a derivable rule {C$\alpha$C$\beta$$\gamma$, C$\alpha$$\beta$, $\alpha$} $\vdash$ $\gamma$. Thus, there exist proofs with a structure like the following:

 A  B  C
  \ | /
    D

It also holds that we have derivable rules for all theorems in this system, and some have some bajillion of antecedents! (by "bajillion" I mean whatever you consider a large number). This implies that there exist theorems with proof-trees like the above far too long to represent with all the resources of planet Earth just in propositional calculus.

So, even within one branch of mathematics producing such a graph leads to problems, because the number of proof methods is by no means small. Producing such a graph across all branches of even this propositional calculus produces difficulties, at least if we allow derivable rules of inference.

That isn't to say that such a graph would come as useless. However, you'll need to fix the rules of inference allowed, and you'll need to disallow derivable rules of inference, and consequently such a graph won't cover all branches of a subject.