15
$\begingroup$

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

$\endgroup$
  • 1
    $\begingroup$ Are you looking for a code repository (for said proof systems), or a "repository" of general proofs (written in English/mathematical notation)? If the latter, have you seen: proofwiki.org/wiki/Main_Page $\endgroup$ – Nicholas Mancuso Aug 8 '12 at 0:45
  • $\begingroup$ I would be surprised to find a structured, comprehensive proof repository. Other than that, every mathematics book is one. $\endgroup$ – Raphael Aug 8 '12 at 7:22
  • 1
    $\begingroup$ @NicholasMancuso Looks promising. The "from" clause in the proof definitions appear to give me what I need. I know the list is not large ~5,000 but as a beginner it may be enough of the map for me to get started. Make it an answer and I will give you an up-vote. $\endgroup$ – Guy Coder Aug 8 '12 at 13:42
  • 1
    $\begingroup$ I'm not sure such a graph exists--there are statements in math that don't necessarily follow directly from a series of other proofs. Many geometric arguments fall in this category. It may be possible to fill them in, but there could be points where no one's bothered to prove the "obvious." If such a graph did exist I think it would be truly massive, both in size and depth. I can't imagine the number of steps to get from ZFC to the quadratic formula, much less Fermat's Last Theorem. $\endgroup$ – SamM Aug 10 '12 at 4:30
10
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ I knew of the Mizar library but did not know about the graph. I will defiantly take a look at this when I get a chance. $\endgroup$ – Guy Coder Sep 10 '12 at 13:30
9
$\begingroup$

ProofWiki contains a decent amount of proofs from various areas of mathematics. It is by no means complete, but is a good starting point for what you want.

$\endgroup$
8
$\begingroup$

Metamath has a large selection of proofs, built right up from their core in propositional logic.

That said, it is painfully lacking in terms of CS theory. Feel free to expand it!

$\endgroup$
  • $\begingroup$ I took a quick look, this looks promising. $\endgroup$ – Guy Coder Aug 14 '12 at 0:13
4
$\begingroup$

See the TPTP archive, Thousands of Problems for Theorem Provers. It is somewhat standard in the field. This is more the "nodes" of the theorem graph you are asking about. Some papers referring to the archive may have explored the edges in this graph.

Note that in the field of ATM, automated theorem proving and assisted theorem proving, the proofs are symbolic and it's not really feasible or plausible to study "proofs in the English language" as you visualize.

However you might learn about Richard's paradox which started out as a language formulation and was later formalized symbolically. It is said to be the inspiration for "antimonies" (contradictions) found in early set theory which historically even paved the way to Gödel's incompleteness theorem.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.