Who is Proofscape For?

  • Proofscape provides a community forum to examine the latest and most exciting advances in mathematics.
  • Have a proof of the Riemann hypothesis? Put it on Proofscape so the community can examine it together.
  • Proofscape is a question-and-answer site where you can get help with a difficult proof, or help others.
  • Pick a proof from a course that you really want to understand well. Adding it to Proofscape (a) solidifies your own understanding, and (b) builds a great resource for everyone else.
  • Proofscape provides a way to examine the structure of proofs, their methods, and their evolution through history.
  • As the library grows there will be increasingly exciting data mining possibilities.

What can you do here?

Expand and collapse proofs and subproofs, lemmas and supporting theorems.
Share your insight by providing an expansion. Or stimulate discussion by requesting one.
Help build the library by encoding a result from the literature in a Proofscape Module.

Explore

Our vision is that eventually any result from the mathematical literature could be looked up and studied in Proofscape. For now we are just starting out, and you can help to build the library.

To locate a result of interest, you can begin at the Library page, or go straight to the proof browser, which is called "Moose," and look up a result from there.

When a result is first opened in Moose, you'll see the theorem diagrammed on the canvas, while in the toolbar on the left you'll see a row that says "Proof" where you can click to open the proof. Try it!

This tool is called the Trail Map, and it lists all the deductions that are currently open on the canvas. It is just one of several tabs that are available, including an Overview tab, and a tab offering direct access to the Library.

As you study the proof, click on any node if you do not quite see how that inference follows. If any expansions are available for that node, they will be listed in the yellow frame in the Trail Map.

An expansion is simply a cluster of nodes and arrows that a user of Proofscape has added to the library, as an explanation of a difficult or obscure inference.

When several different expansions are available for the node you've selected, they'll be sorted by the number of stars they've been awarded by users of Proofscape. This is an "up vote" you can award to expansions that you like.

You can open an expansion by clicking its row in the Trail Map, or you can click the icon on the yellow frame to open a separate page where you can compare all the available expansions.


Share

Besides representing existing theorems and proofs from the literature, one of the main purposes of Proofscape is to let you provide as well as request expansions on inferences that you feel could use some further explanation.

Suppose you want to provide an expansion on a certain node. When you select that node in Moose, the 'Provide' button will activate in the left-hand toolbar.

If you are the first to provide an expansion for this node, then the module editor will open directly when you click 'Provide'. Learn how to write modules here.

If however this node already has any expansions, then you'll first be brought to a page where you can browse all of them. At the bottom of that page you can click a button to provide a new expansion, if you think you have a different way to see it.

If instead you'd like to request that somebody else provide an expansion for a node whose inference is unclear to you, you can select the node, and click the 'Request' button. You'll be taken to a page where you can describe your request.

All existing requests can be viewed by navigating to the Requests page, where you can see what kinds of questions people are asking, and offer an expansion in answer.

Build

Building the library means coding representations of results from the literature, as well as providing expansions. Every deduction in the library is encoded in a Proofscape module.

Proofscape modules have their own syntax, which you can learn here.

We talked above about how you can provide an expansion. If instead you want to code a new result from the literature, you can initiate that from the Library page. Simply navigate to the work in question, then click the button that says, 'Transcribe it'.

As for editing existing modules, you'll find a pencil icon on each row in the Trail Map. In addition there is a talk icon that takes you to a page for free discussion of each module. This allows you to make comments, as well as suggest changes to modules that have been closed for editing, or expansions that are not your own.