README.md

math-o-matic

main page · docs

math-o-matic is a program that lets you create a proof system and prove its theorems, in the most rigorous way possible. Its aim is to make it easy to read and write rigorous mathematical proofs. You can take a look at the current system by clicking on one of the links at the bottom of the main page.

Setting up the environment

Install git & Node.js and run:

git clone https://github.com/math-o-matic/math-o-matic.git
cd math-o-matic
npm run install-all
npm run build

Creating your first proof system

Suppose that you want to create a simple proof system about the natural numbers characterized by the axiom

• A1. nat(0),

where nat(n) means "n is a natural number," and the inference rule

• R1. From nat(n), infer nat(successor(n)),

and prove that 2 is a natural number, where 2 is defined as successor(successor(0)).

Create the file math/com/example/Natural.math and write:

package com.example;

system Natural {
    "The proposition type."
    type prop;

    "The object type."
    type obj;
    
    "The primitive notion that given an object, tells if the
    object is a natural number or not."
    prop nat(obj o);

    "The successor of a natural number."
    obj successor(obj o);

    "The natural number 0."
    $0$
    obj zero;
    
    "The natural number 1."
    $1$
    obj one = successor(zero);
    
    "The natural number 2."
    $2$
    obj two = successor(one);

    "Axiom A1."
    axiom nat_zero() {
        nat(zero)
    }

    "Inference rule R1."
    axiom nat_successor(obj n) {
        nat(n) |- nat(successor(n))
    }
    
    "2 is a natural number."
    theorem nat_two() {
        /*
         * nat_zero() proves nat(zero), and nat_successor(zero)
         * proves nat(zero) |- nat(successor(zero)). The left associative
         * `>` operator then proves nat(successor(zero)) from the two
         * operands, then the next `>` proves nat(successor(one)) from the
         * operands nat(one) and nat(one) |- nat(successor(one)). The
         * `as` operator makes sure that nat(successor(one)) and nat(two)
         * are the same thing and changes the displayed formula from
         * nat(successor(one)) to nat(two).
         *
         * Check out the proof explorer from the web page to watch this
         * in action.
         */
        nat_zero()
        > nat_successor(zero)
        > nat_successor(one)
        as nat(two)
    }
}

From the web directory run npm run serve and open the displayed link in the browser. Click on system com.example.Natural to see the rendered proof system. For example the theorem nat_two will be rendered as follows:

The green color indicates that the math-o-matic program succeeded to validate the theorem or the axiom.

The proof system we're building

Otherwise you can take a look at & contribute to the proof system we're currently building, located in the /math directory. Our proof system is based on natural deduction and the Morse–Kelley set theory and managed to prove theorems like:

• 1 + 1 = 2 (std.Natural.one_plus_one_is_two),
• Recursion theorem (std.Natural.recursion_theorem),
• The principle of mathematical induction (std.Natural.induce),
• Cantor's theorem (std.Function.cantor),
• Schröder–Bernstein theorem (std.Natural.schroeder_bernstein).

More stuff

• Find more math-o-matic code under the /math directory.
• Refer to the documentation to learn how to write proofs.
• math-o-matic language support for Visual Studio Code can be found here.