What is Prooftoys?
Prooftoys is a set of resources for learning and using principles of precise reasoning. This is the reasoning of mathematics, but today it applies to many fields — very broadly to much of computing, but also to many other fields, often through mathematical modeling and other forms of mathematical analysis.
The Prooftoys system has been designed specifically to be approachable for beginners who may have little background in mathematics and perhaps no background at all in formal logic. It exists to be an understandable and enjoyable road to learning and applying these super-powerful tools through an embedded graphical user interface that helps you construct understandable and correct proofs with no holes and no handwaving.
Ways to start
-
Visually: with logic through pictures, an introduction to some universal basics of logic. These are interactive diagrams with explanation, and truth tables, to support your intuitive sense of concepts such as and, or, not, and implies).
-
Hands on: with an extensive and self-contained Natural Numbers Game tutorial that takes you step-by-step through proofs of fundamental properties of numbers, with background, hints, and tips for taking on its challenges; and an assortment of logical puzzles.
-
In depth: through the documentation of the logic and the system, including a quickstart demonstration of the Prooftoys proof builder.
Need some reasons?
Simplicity is the ultimate sophistication. – Leonardo da Vinci
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.