(Prove It)(Yes You Can)
Welcome to Prooftoys, an online tool for exploring mathematical reasoning and website with resources for learning. The overriding design objective of Prooftoys is to drastically reduce the learning curve for working with precise, automated reasoning. Here you can:
- Introduce yourself to basic logic concepts through pictures.
- Get acquainted with the automated logic used here.
- Dig into proofs created and verified by Prooftoys. Understand in detail or just browse.
- Eventually you may experiment with building your own proofs with the online tool.
The core of the system is proudly free and open source software, hosted on GitHub.
Logic through pictures
This site has explanations of concepts at work in mathematical logic and the Prooftoys system, with interactive pictures resembling these:
The automated logic
Prooftoys applies the kind of logic used in several popular tools for specialists, but presents it with the overriding goal of being as approachable to beginners as possible, and to make statements in the language familiar to users of ordinary math textbooks. Next steps in this direction -
- Concepts of the Prooftoys logic.
- The logical language of Prooftoys.
- The rules of the game as played with Prooftoys.
Digging into proofs
With Prooftoys you can view and study completed proofs. This website contains “live” displays of many of them, like this:
Some are proofs of basic facts about numbers, derived from classic axioms. Others are useful theorems of pure logic that can apply to any field of math. You can view the facts and their proofs, which are all worked out rigorously and computer-verified. If a step is not clear, you can “drill down” into the details, all the way down to the most basic axioms and inferences.