Proofscape is a collaborative visual library of mathematics. It's also a historical catalog of the origins of our subject. It permits us to study not just some proof of each theorem, but each of the known proofs, situated within the full theoretical development to which it belongs. The classic texts in which the subject was born give us more than just theorems, proofs, and definitions; each one provides an entire rendition of a theory, a way of structuring it, of building up from the initial theorems to the high points of the theory. By comparing the ways its original authors conceived of the subject and wrote its proofs, we deepen our insight into the truth behind the theory.
Proofscape gives us a way to represent the deductive structure of theories with rigor, but without going to full formalism. The library will yield fascinating opportunities to mine the structure of proofs in practice, and, with community involvement, has the potential to grow quickly since modules are easy to write. The syntax can be learned in an afternoon, and a moderate sized proof can be encoded in under an hour.
Proofscape takes a unifying view in which mathematical discourse proceeds as a hierarchy of nested deductions. A theorem statement is a deduction: it states something which has been deduced. But the statement demands further explanation, and that is why a proof is offered. The proof is another deduction, nested inside the theorem, and it fills in the deductive gap between the premises and the conclusion of the theorem.
Meanwhile every proof is pitched by its author at some imagined audience, and while it may be just right for some, others may find that it does not explain enough. In other words, the proof itself may leave inferential gaps which could be filled in with more detail. In this way, a single inference within a proof is like a "mini theorem," which itself may demand proof. For this yet another deduction can be offered, deepening the deductive hierarchy by yet another level.
On the other hand, after reading and understanding one of the deeper deductions in this hierarchy of explanations, a reader may wish to hide it, and return to the big picture into which that deduction fits.
The purpose of Proofscape is to allow all people interested in mathematics to request and provide recursive explanations of existing proofs, and to explore these explanations interactively.
We hope to see vast tracts of the existing mathematical literature represented in Proofscape, and we hope that users will provide expansions where they see fit, as well as taking full advantage of the social aspects of the site, including both the expansion request feature, and the discussion pages.
For more about the purpose and capabilities of Proofscape, please visit the tour page.