Hands-on with Prooftoys
Contents
Proving
Mathematical reasoning — in other words proof — is the core of everything Prooftoys does. It can be explicit, visible to you step-by-step, or behind the scenes. The hands-on pages show simple and useful forms of reasoning that you can use anywhere in your larger mathematical journey.
Simplification
Simplification is a basic and powerful tool that we often take for granted in mathematics. It is just as important and valuable for computer-supported proving as for doing math by hand.
-
Super-simple puzzle that can be solved with simplification alone. Gives a taste of simplification as a mathematical super-power.
Textbook-style proof (“forward” proof)
-
Direct proof uses a familiar and simple process, starting from things already known to create new knowlege. It is a great way to start with proof in Prooftoys. Apply classic proof techniques here to prove essential properties of zero.
-
A Fake Proof that
1 = 2
This longer forward-style proof uses simple algebraic manipulations, showing one way proper formal reasoning wins out over fallacious informal reasoning.
Goal-directed proof
Goal-directed proof is often used with computer proof assistant software. Having a stated goal enables the Prooftoys proof builder to highlight assumptions in the current result that still need to be proved to reach
-
A short goal-directed proof with a full interactive demo walkthrough. Uses universal and existential quantification. A fine starting point for working with Prooftoys and goal-directed proof.
-
Sometimes known as the “drinker paradox”. Another goal-directed proof using quantifiers.
-
How long is a lunar? (upcoming)
Proof by induction — extended tutorial
-
Extended tutorial that develops some basic propertiess of the natural numbers from first principles. Uses mathematical induction and goal-directed proof throughout. Note: A simple example such as the Country Music Theorem can be an equally good starting point for working with Prooftoys, but this tutorial also introduces proof by induction and takes you through several proofs.
Proof builder tool
-
Just the tool by itself, a playground for trying whatever you like.
Solving
Algebra
(work in progress)
Solutions to typical algebra problems — or solutions to sets of
equations — are typically mathematical statements equivalent to the
problem statement, but in a simpler or more useful form such as x = . . .
. When solving for multiple variables, the prototypical result is
an “and” that mentions each of those variables, like x = . . . & y = . . .
. If there are multiple solutions, the result is an “or” like x = . . . | x = . . .
.
Everything here, from the tactics to the presentation, is not nearly as polished as the rest of the site, but feel free to take a look. If you would like to see a worked solution to a problem, press the “Solve” button.
- Linear equations with 1 variable
- Simultaneous linear equations
- Simultaneous with no solution
- Finding a common denominator
- Rational functions including demo of division by zero