Metamath is project that attempts to describe mathematics from ground up starting from very simple axioms, following very simple rules, building more and more complex theorems on top. While having everything machine checked using a very simple verifier. It has one of the largest collection of over 30,000 theorems and their proofs. Forematics is a Metamath verifier written in Nim.
Metamath is a pure math language that looks like this:
⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
Forematics is build like any simple interpreter with with a tokenizer, parser and an eval loop. It has ability to define constants, variables, axioms and theorems (kind of like functions). It then uses a simple interpreter to verify that all theorems based on starting axioms are valid.
All "evaluation" is done by the substitution rule. There is no other built in concepts. Using the substitution rule it derives all concepts like what numbers are. Including how parentheses (), if-then, +, -, and all other math operators. It only proves 1 + 1 = 2 after defining 11086 other theorems and it proves Pythagorean theorem z² = x² + y² after defining complex numbers after doing 24464 other theorems.
Forematics can't be used to compute, derive or solve equations, its not a Computer algebra system but maybe a small part of one that only deals with proofs... and very simple and constrained proofs at that.
Forematics is fast, because Nim is fast, can verify and prove 30,000 profs in 21 seconds.
Cool.
I know nothing about how a verifier can be implemented. Could you provide more information?
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
Now lets prove that:
t = t
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)
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.
Sorry I don't know much about Lean. Big different is that Lean is big, while the metamath proof verifier in Nim is only 500 lines. Lean defines many of the mathy things we expect, while metamath defines nothing except substitutions. Both are trying to encode mathamtaics and verify proofs using a computer.
There is a list of 100 theorems, almost like "proof acid test" that every verifier is trying to get too.
See this article: https://www.cs.ru.nl/~freek/100/
The stats in the article are:
HOL Light ...... 86
Isabelle ....... 86
Coq ............ 75
Metamath ....... 74
Mizar .......... 69
Lean ........... 61
ProofPower ..... 43
PVS ............ 22
nqthm/ACL2 ..... 18
NuPRL/MetaPRL .. 8
So Lean has proven less theorems than Metamath and is way more complex.