If you want to learn more about mathematical verifiers I recommend taking a
look at the metamath book: <http://us.metamath.org/downloads/metamath.pdf>
The philosophy of Metamath is:
> Metamath “knows no math;” it just provides a framework in which to express
> mathematics. Its language is very small. You can define two kinds of symbols,
> constants and variables. The only thing Metamath knows how to do is to
> substitute strings of symbols for the variables in an expression based on
> instructions you provide it in a proof, subject to certain constraints you
> specify for the variables.
Here is an example of a simple proof from the book:
Lets start with these axioms:
(A1) (t = r → (t = s → r = s))
(A2) (t + 0) = t
Run
Now lets prove that:
t = t
Run
The proof steps are:
1. (t + 0) = t (by axiom A2)
2. (t + 0) = t (by axiom A2)
3. ((t + 0) = t → ((t + 0) = t → t = t)) (by axiom A1)
4. ((t + 0) = t → t = t) (by modus ponens applied to steps 2 and 3)
5. t = t (by modus ponens applied to steps 1 and 4)
Run
It's just moving symbols around with simple rules. It knows no math. Just
basically a `.replace()` contorted and used in different ways.
See page 39 of the linked PDF for more info.
