Show Nim: Forematics is a Metamath verifier written in Nim.

[treeform]

[Metamath](http://us.metamath.org/) 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](https://github.com/treeform/forematics) is a 
[Metamath](http://us.metamath.org/) verifier written in Nim.

Metamath is a pure math language that looks like this:
    
    
    ⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
    
    
    Run

Example of an Axiom: [Existence of reciprocal of nonzero real 
number](http://us.metamath.org/mpeuni/ax-rrecex.html).

## Forematics

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](http://us.metamath.org/mpegif/1p1e2.html) `1 + 1 = 
2` after defining 11086 other theorems and it [proves Pythagorean 
theorem](http://us.metamath.org/mpegif/pythag.html) `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](https://en.wikipedia.org/wiki/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.