"We all believe that mathematics is an art. The author of a book, the lecturer in a classroom tries to convey the structural beauty of mathematics to his readers, to his listeners. In this attempt he must always fail. Mathematics is logical to be sure; each conclusion is drawn from previously derived statements. Yet the whole of it, the real piece of art, is not linear; worse than that its perception should be instantaneous. We all have experienced on some rare occasions the feeling of elation in realizing that we have enabled our listeners to see at a moment's glance the whole architecture and all its ramifications. How can this be achieved? Clinging stubbornly to the logical sequence inhibits the visualization of the whole, and yet this logical structure must predominate or chaos would result."
--- Emil Artin, 1953
"...if we estimate the size of a work, not from the number of its pages, but from the time which we require to make ourselves master of it, it may be said of many a book that it would be much shorter, if it were not so short. On the other hand, as regards the comprehensibility ... we may say with equal justice: many a book would have been much clearer, if it had not been intended to be so very clear. For explanations and examples, and other helps to intelligibility, aid us in the comprehension of parts, but they distract the attention, dissipate the mental power of the reader, and stand in the way of his forming a clear conception of the whole...
--- Immanuel Kant, 1781

Exploring Theories

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.

A Digital Catalog

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.

Recursive Structure

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.

Our Vision

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.