I am self-learning proof assistants and decided to start on some basic proofs and work my way up. Since proofs are based on other proofs and so form a hierarchy, is there a repository of the hierarchy of proofs?
I know I can pick a particular proof-assistant and analyze its library to extract its hierarchy, however if I want to find the next proof in a chain to prove, I can't when it is not in the library.
In my mind I picture a graph, probably a DAG, of all of the known mathematical proofs that can be expressed using English statements, not proofs using pictures. This would be the master map (a map in the sense of starting at one point and traveling to another point via intermediate points), and for a particular proof assistant, one would have a subgraph of the master map. Then if one wanted to create a proof using a proof assistant found on the master not on the subgraph, by comparing the two graphs one could get an idea of the work needed to create the missing proof(s) for the proof assistant.
I am aware that mathematical proofs are not necessarily easily convertable for use with a proof assistant, however having a general idea of what to do is much better than none at all.
Also by having the master map, I can see if there are mulitple paths from one point to antoher and choose a path that is more amenable for the particualr proof assistant.