Docs Mission About

Hands-on with Prooftoys

Proving

Simple puzzles and examples

  • The repetitious number

    Super-simple puzzle that can be solved with simplification alone.

  • 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.

  • A Fake Proof that 1 = 2

    This proof uses simple algebraic manipulations, leading to a result that illustrates what fallacious informal reasoning can lead to in a system that reasons properly

  • How long is a lunar? (upcoming)

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. 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.

Tool

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.