What is Prooftoys?
Prooftoys is software and a set of resources for learning and using the principles of logical reasoning.
The Prooftoys system has been designed specifically to be approachable for beginners with little background in mathematics and even no background at all in formal logic. Its goal is to provide an understandable and enjoyable road to learning and applying these super-powerful tools through a graphical user interface that helps you construct understandable and correct proofs with no holes and no handwaving.
The Vision
On the one hand, Prooftoys is for learning core ideas of mathematical proof, general concepts of reasoning rather than cookbook procedures, in a way that is approachable to ordinary people.
In a larger sense though, Prooftoys is an effort to find better ways to learn these great ideas in our modern era. Far too much of math education is still about people doing procedures that may have been useful three hundred years ago, but pointless to do by hand now.
Computers can do the procedures for us, but without the concepts we are still lost. Luckily, there are now powerful systems of mathematical reasoning that are based on simple principles used throughout ordinary high school mathematics, and Prooftoys uses one of these for all of its reasoning.
Prooftoys is an example of a new way of introducing mathematics where the computer does things it is very good at, and human beings learn concepts and key ideas. It also aims to do this in a way that is stimulating and interesting, not boring and a waste of time. It is the result of ongoing experimentation, and will evolve based on the experience and input of people like you.
What can it do for me?
-
Build your skills and develop your understanding of rock-solid reasoning.
-
Grow your appreciation of the power of reasoning from fundamental principles.
-
Demonstrate solving traditional school math problems through proof.
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 important properties of numbers starting from a small handful of fundamental principles. This includes background, hints, and tips for taking on its challenges
Logical puzzles are also here, illustrating principles of proof, with a potential surprise or two.
There are also demonstrations of solving basic algebra problems with the help of the computer. Prooftoys handles algebra problems as proofs, so the steps are guaranteed to be mathematically correct.
-
In depth: through the documentation of the logic and the system, including a quickstart demonstration of the Prooftoys proof builder.
Why try Prooftoys?
Simplicity is the ultimate sophistication. – Leonardo da Vinci
User interface. Prooftoys works entirely through a Web-based point-and-click graphical user interface. Most things you do are based on suggestions based on your selection of a step or expression. It lets you change your mind as much as you like, encouraging you to “play around” with your proofs.
Simplicity. The logic used by Prooftoys has also been chosen specifically to be useful to 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. 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 proofs are 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 advance.