A Logical Tool for Mathematics

A modern road to the world of mathematics
A system of deduction built on simple concepts
Explicit, practical, and transparent
A user interface that makes smart suggestions and prevents errors

Is it for You?

Are you comfortable using basic algebra?
Desire a stronger grasp of mathematical reasoning?
Check it out.

Peek

Examples and video preview that demonstrate the principles and the tool.

Try

Experiment with textbook-style math problems and simple proofs.

Learn

Detailed information about the logic and how to use the system.

A Live Medium

The reasoning is right in front of you.

Textbook-style presentation

Computer deduction behind each step

All assumptions and the problem statement are fully laid out.

Each step has a number and a description.

Details are available when you need them.

Open up a step to see the details to any level.

Even details of extensive simplifications are just a click away.

In Prooftoys, theorems and useful variants are considered "facts", and can be looked up for use as proof steps. You can view the proof of any fact just like details of other kinds of steps.

Step 14 here is a fact proved from another fact using commutativity of addition.

Take a look.

Smart

The user interface is syntax-aware.

You select a step or part to transform.

Only meaningful selections are possible.

For completed steps, the display can highlight the term that was transformed, and tries to also highligh the result of the transformation.

Try it.

The menu suggests steps that can apply to your selection.

Suggestions appear in the menu

Inapplicable actions are filtered out

Freely choose what to do next at all times

The logic ensures correct reasoning

Simple and Approachable

All reasoning ultimately uses equations, as below. The "==" symbol is for logical equivalence (equality of truth values).

Numbers – (x * y = 0) == (x = 0) or (y = 0)

Truth values – (A and A) == A

Functions – f = g == forall {x. f x = g x}

Builds directly on basic algebra

Minimal additional concepts

Many higher-level inferences are simple combinations of the basic kinds of inferences

Learn how.

In memoriam
Peter B. Andrews
1937 - 2025

Professor Peter Andrews developed the formulation of simple type theory (or "higher-order logic") that he called Q₀. Everything here is based on that system, and the internal development of the logic here closely follows his.