What is Prooftoys?
Prooftoys is a set of resources for learning the principles of precise reasoning – logic and mathematical proof, tailored specifically for beginners with little background in mathematics and no background in formal logic. It exists to be an enjoyable and rewarding road to learning and applying these powerful tools, and includes an embedded graphical tool that helps you construct understandable and correct proofs with no holes and no handwaves.
Get introduced
-
Tour the picture gallery that introduces basic “boolean” logic. These are interactive Venn diagrams with explanation, and truth tables – a point of view on “propositional” logic (e.g. and, or, not, and implies).
-
Learn the language of Prooftoys.
-
Understand its simple, practical, efficient system of deduction.
Dive straight in
-
Quick start on the proof builder page.
-
Check out examples of rigorous proofs. You can view all of the theorems in the system – both theorems of logic and the real numbers. Understand them in detail or just browse. The same techniques are available for you to use in the proof builder.
Need some reasons?
User interface. Prooftoys works entirely through a Web-based point-and-click graphical user interface. You select a step or part of a step. Prooftoys offers you suggestions and lets you change your mind as often as you like, encouraging you to “play around” with your proofs. If used well, suggestions benefit from recognition being easier than recall.
Simplicity. The logic used by Prooftoys has also been chosen specifically for beginners. For example its single rule of inference is just a modest generalization of what is taught in any high school course in basic algebra.
Statements in the logic are simply formulas with constants, variables, and functions. Prooftoys reduces the number of concepts to a minimum, with just a little automation for convenience. There is no need to learn a separate proof language with its own syntax and vocabulary.
Flexibility. Prooftoys is as well-suited to solving problems as to proving theorems. For example it easily works backward from the statement of a theorem or forward from the givens of a problem.
Familiarity. Prooftoys works to present its mathematics in familiar, textbook-like style. For example type conditions are stated as assumptions rather than type annotations, and the result of division by zero is not a number. Proofs show up in a familiar textbook style as a list of proved statements, each derived from the ones before it.
Transparency. Prooftoys makes the details of every step in every proof available in the proof builder and all proof displays. A click lets you drill down into the details of any step, to any depth.
Resources. With this website you can see how it is done or learn about the ideas behind the logic to build your skills and confidence in solving mathematical problems through proof.
Prooftoys is for learning. If you need more power or larger scale, you should look at more established proof assistant systems, which support:
- Large collections of theorems
- Editing entire mathematical theories
- Strong automation
The Prooftoys website and its software are ongoing experiments in creating computer aids to help human beings do mathematics. Its knowledge of mathematics is quite limited, but we aim to grow it as users become more advanced and ask for more.