Welcome!

Welcome to the Prooftoys edition of the Natural Numbers Game, a series of puzzles in which you build up mathematical knowledge about numbers step by step with computer guidance. As you take on the challenges of the game you build skills in creating 100% correct mathematical proofs.

What is this about?

You will start with just the bare essentials of knowledge about the natural numbers (the “counting numbers”, 0, 1, 2, 3, and so on up from there) and work your way up to more powerful knowledge through mathematical proofs.

The structure of this game is largely a clone of the admirable original Natural Number Game tutorial developed in England at Cambridge University using the Lean Theorem Prover. This edition uses the Prooftoys proof assistant, with its focus on graphical user interaction, simplicity, and ease of use for beginners. While it knows far less mathematics than research-grade proof assistants such as Lean, the logic of Prooftoys is capable of supporting advanced university-level math.

Will it be hard?

If you have studied basic high school algebra, you have the concepts you will need! In fact it turns out that there are fundamentally only two ways in Prooftoys to go from one true statement to another, and these are both part of ordinary high school algebra. We will review the principles with you in the next few sections, and Prooftoys will provide you with the guidance and suggestions to help you succeed.

Your first mission, should you decide to accept it, is to prove that 0 = 0 — about as simple as it gets.

The tiny one-step proof of this will use the principle that anything is equal to itself. As trivial as it is, it shows a great deal about using Prooftoys.

What is this?

In front of you is a Prooftoys proof editor. It displays a proof in progress, and lets you interactively add to or modify the proof, experimenting with different proof steps and approaches.

You should see the beginning of a proof, with just one line. If not, click on “Clear work”, then confirm that you want to clear your work. The initial statement in this case is 0 = 0 => 0 = 0, which Prooftoys proves internally.

The pieces

This is a conditional statement because of the double arrow (=>) in the middle, which is the conditional operator. You can read a conditional statement A => B as A implies B, or if A then B. Items on the left side of a conditional are considered assumptions. This statement has only one assumption: 0 = 0. The part of the statement after the conditional operator we will call the conclusion. All of these, and any meaningful part of a a statement such as the assumptions and the conclusion we will call a term.

We say that this statement has the form A => A because it has the same statement on the left and on the right of the => operator. Put another way, if you replace both of the A’s with 0 = 0 you get 0 = 0 => 0 = 0. Replacement of all occurrences of a variable with the same term is substitution – one of the two fundamental ways of getting from one true statement to another in the logic of Prooftoys.

Taking your first step

First steps are big milestones! This proof will have just one step. Start by selecting the assumption, the first 0 = 0. As you hover the mouse cursor over different parts of the statement they will highlight to show that they can be selected. Click to confirm the offered selection like this (Hover the mouse cursor to see a demonstration.)

Next look at the menu down at the bottom of the proof editor. If the “Basic” section of the menu is not already displayed, show it by pausing the mouse cursor over the word “Basic”.

The menu offers you choices for the next proof step. You will want the menu item that starts with ➭ T. This arrow at the beginning of a menu item means that the selected term will be transformed into T, for true. Many typical proof steps are like this, transforming an assumption into some other form.

Go ahead and select that menu item. Now you should see a second step in the proof editor display, and the words “Proof complete” at the top of the proof editor area. When Prooftoys proves that an assumption is true, it normally drops it from the assumptions. In this case there are no more assumptions, so we are left with just the desired result – the goal statement.

The words “Proof complete” appear at the top of the proof editor display, confirming that your mission is accomplished.

This one proof step illustrates both of the basic operations Prooftoys uses to get from one true statement to another true statement: substitution as already described, and replacement of a term with some equal term. In this step, Prooftoys uses the fact that (x = x) == T to replace 0 = 0 with T. It then drops the true assumption T from the assumptions, leaving just the conclusion.

This combination of substitution together with replacement is known as rewriting, our most widely used type of proof step. You will also use some other kinds of combination steps in playing the Natural Numbers Game, but don’t worry — they are all just conveniences to help make your journey easier.

So it is fair to say that this simple one step proof sets the stage for all reasoning in Prooftoys!

➪ Next

About the Proof Editor

Here is a quick visual reference to the parts of a proof editor. The labeled parts are:

1. Proof display. This shows the steps of your proof so far. It lets you select steps or parts of steps, or delete steps easily.
2. Action menu. This menu is dynamic based on the current selection in the proof display. Selecting items here is the way you develop and edit proofs.
3. Goal statement. This shows what you are trying to prove. If it has the form A => B, A has the expected assumptions for proving the conclusion B.
4. Copy text. This lets you copy the most recently-selected term as text.
5. Clear work. Use this button to restart the proof from the beginning.
6. Checking this box gives the developer permission to generate detailed traces of your activity for research purposes, to improve the website and the proof editor. See the privacy information page for details.

➪ Next