The problem of the repetitious number
This puzzle comes from the book “My Best Mathematical and Logic Puzzles” by the legendary Martin Gardner, author of numerous books of entertaining and puzzling mathematics and, for 25 years, the Mathematical Games column in Scientific American magazine.
It is problem 20 in the book, a little mathematical parlor trick. In this parlor trick you ask spectator A to write down any threedigit number, then to copy the number to a new piece of paper, followed by the same digits again, making a sixdigit number. Without looking, instruct spectator A to pass the paper to spectator B without revealing the number to you.
Spectator B is to divide the resulting number by 7, and then pass the result to a spectator C, who divides the result by 11. (Tell them not to worry, there will be no remainder!)
Spectator C passes it to yet one final spectator. This last spectator is to divide the result by 13 and then read the resulting quotient. The result will be the original threedigit number.
Problem: Prove that this trick always works regardless of the initiallychosen number.
Hint: The key to solving this problem is finding a simple mathematical statement of it.
Solution
The key to this problem is that writing down a threedigit number and then making it into a sixdigit number by appending the same three digits has the same effect as multiplying by 1,001.
So we can ask, is it true that
1001 * x / 7 / 11 / 13 = x
?
Here is a solution built with Prooftoys.
The steps. A proof consists of a sequence of steps connected by inference rules, each producing a new step. In this proof we have:

“Consider” – we start by “considering” the expression in the problem statement. Just under the hood, the full statement here is that
1001 * x / 7 / 11 / 13 = 1001 * x / 7 / 11 / 13
, and this is true because anything is equal to itself. The full content of the step is a statement that the term is equal to itself. This step was created using the menu, selecting “consider”, and typing in1001 * x / 7 / 11 / 13
.Viewing the whole step. If you hover the mouse over the small blank space between the step number and the expression for this step, Prooftoys will display the entire step for you. In general, if you hover the mouse over this area, or an ellipsis (" … “) in this part of a step, Prooftoys will show you all of the parts of the step.

“Simplify” – select the entire step by clicking on the checkbox. Then select “algebra: simplify” from the menu that pops up.

“Standard form … " – select the term
1001 * x / 1001
, then pick the item “algebra: to form k * x” from the menu that pops up. 
“Display fully” – This step does no inference, but causes the system to show all parts of its input step.
The display. Prooftoys often just displays an ellipsis (” … “) if part of a step is the same as in the previous step. If you hover the mouse cursor over the " … “, Prooftoys displays the entire step without omissions. Or for step (1), hover over the blank space after the step number.
If you hover the mouse cursor over one of the step numbers, Prooftoys will highlight the part of the step that it worked on to get this one. If it worked on the whole step, it highlights just the number of the step it used as its input.
What about R x => . . .
? This means that if x is a (“real”)
number, then the statement is true. The R
is for “real”. In
slightly different words, it expresses the usual assumption that
x
is a real number.
Try the steps yourself
Can you build the same proof yourself from just the given statement? Here is a workspace you can use to do the experiment.
Seeing details
Prooftoys encourages you to dig down into any step to see details for it. To see the next level of detail, click on the blue text in the description of the step, in this case the text starting with “standard form”. The display then expands vertically to show you another level of detail. Click on the same text again or on the box labeled “hide” to hide the details again. If there are many levels of detail you can repeat this process on steps in the detailed display.
If a step has the word “use” in its description, it means the step applies a rewrite rule.
Is there an easier way?
If you are good at math and rarely make mistakes as you work a problem, you probably find it easier to solve problems like this in your usual way, and then you don’t have to learn a new tool.
On the other hand, Prooftoys has a complete set of rules for reasoning, and it won’t goof if it gets a new kind of problem.
There is a quite different breed of computer tool for solving typical textbook math problems, and they are called “computer algebra systems”. With one of them you may be able to just enter a statement of the problem, and it will crank out the answer. For many kinds of problems they are much more capable than Prooftoys, but you will not learn nearly as much about proper mathematical reasoning by using one, and they are not built to work collaboratively with the human user as interactive proof assistants such as Prooftoys are.
What’s next?
There are more logical puzzles and examples in the “handson” section.
And if some things here interest you, please check out the “about” page for ways to get in touch.