What is Prooftoys?
Simplicity is the ultimate sophistication. – Leonardo da Vinci
Prooftoys is software and a set of resources for applying mathematical reasoning.
It has been designed to be approachable for beginners. You won’t need a background in mathematics or logic. The graphical user interface will work with you to:
- construct correct proofs with no holes and no handwaving, and
- solve math problems easily through proof.
Reasoning in Prooftoys is based on principles from basic algebra. These same principles extend to higher mathematics as well.
Ways to start
-
Pictures: The logic through pictures section introduces 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 illustrate principles of proof, with a potential surprise or two.
Basic algebra problems solved through proof. Be assured that your steps will be mathematically correct.
-
Documentation: Read about the mathematics and the system. Watch a video demonstration of the Prooftoys proof builder.
Reasons to try
-
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.
How?
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.
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.