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

[treeform]

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
    
    
    Run

So Lean has proven less theorems than Metamath and is way more complex.