(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:

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:

sample logic graphic

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 -

Digging into proofs

With Prooftoys you can view and study completed proofs. This website contains “live” displays of many of them, like this:

sample proof display

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.

Building your own

  • The more finished version of the proof builder is targeted for solving simple equations, at the companion Mathtoys site.
  • For the boldest, dive into building your own proofs with the proof builder. This tool has some rough edges still, though it will only do correct inferences.