Given a proof for a result, one could denote the proof as a node on a graph, and then draw arrows to the node from axioms and previous results that the proof uses, and then draw arrows from the node to results that the result is used to prove. The sources of such a graph would be mathematical axioms and the sinks would be results which do not yet have corollaries. This is related to the facts that finite categories can be drawn as directed graphs and that proofs form a category.

Question: Is there an existing ontological/relational database somewhere that attempts to make use of such an idea to formally encode some of present-day mathematics?

It can often be difficult to fully trace all of the logical dependencies of a given result. For example, how can one show whether existing proofs of the Implicit Function Theorem use the Law of the Excluded Middle or not? Rather than spend a couple of days going through tens of textbooks and trying to parse their proofs, not for their content but just to see what assumptions they are using, wouldn't it be easier to ask a computer to do that task?

Such a system for tracking the logical dependencies of known proofs for existing theorems could be useful not only for beginners ("What important theorems use the completeness property of the real numbers? I'll check the database."), but it could also be useful for constructivists or intuitionists who want to keep track of which existing results make use of the Axiom of Choice or the Law of the Excluded Middle. And maybe it would be possible to use a sufficiently complete database to run tests to see whether the foundations of mathematics are consistent? I don't actually know, but it sounds on a naive level something that would be useful, even if it would take a long time to build.

Note: I am not sure what to tag this question or if it is on-topic.