Docs Mission About

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.

Proof builder tool

Background: The proof builder uses a formal mathematical language of the same kind used in textbooks that express mathematical ideas formally. To work well with the proof builder, you will need to develop a good working relationship with this language and its meaning. The detailed tutorials offer some explanations about the way they use this language, and you can learn more in the Prooftoys documentation.

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.

  • The repetitious number

    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

    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.

  • Proof by cases

    A simple example of proof by cases, showing a fact about multiplication by zero.

  • A Fake Proof that 1 = 2

    This longer forward-style proof shows 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

  • Country Music Theorem

    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.

  • The Drinking Theorem

    Sometimes known as the “drinker paradox”. Another goal-directed proof using quantifiers.

  • How long is a lunar? (upcoming)

Proof by induction — extended tutorial

  • The Natural Numbers Game

    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.

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.