[Solved]: Is there a repository for the hierarchy of proofs?

Problem Detail: 

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.

EDIT

In searching I found something similar for mathematical functions. I did not find one for proofs at the NIST

Asked By : Guy Coder

Answered By : Realz Slaw

The Mizar system is a huge repository of math proofs. See the wikipedia page and the official website.

of all of the known mathematical proofs that can be expressed using English statements

From wikipedia/Mizar_system#Mizar_language:

The distinctive feature of the Mizar language is its readability

Proofs are written as articles, of which there are more than a thousand articles, and more than 50,000 proven theorems. The wikipedia page mentions some interesting ideas of the "QED manifesto", and how Mizar might be on its way to accomplishing this.

• A huge graph of the Mizar library.
• This paper might also be helpful: Combining Mizar and TPTP Semantic Presentation Tools

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/3086