Hi All, Inspired by Marnix Klooster's recent post on a Zig verifier, I decided to restart my plan from several years ago to write a metamath verifier in Lean. Lean 3 is interpreted, and it was so slow that I decided to abandon the project, but lean 4 compiles to C and so it has quite competitive performance. It's not quite as impressive as smm3, but it can compile set.mm in 10-12 seconds so I'm quite happy with it.
One of the advantages of writing in lean is that verification of the verifier becomes in principle possible. Right now Lean 4 is much more well suited to writing programs than proving theorems, but I expect that this will change in time, and there are a few theorems already in the file, mainly to avoid some bounds checks. As far as features are concerned, it's pretty bare bones (and if it is to eventually be verified it is probably best to keep it bare bones). It can handle compressed and normal proofs, and all the official MM stuff except for $[ $] import statements. https://github.com/digama0/mm-lean4/blob/master/Metamath.lean Mario Carneiro -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSu-QVTE_X_k3V60MqL1YSYNa7ZQQW4FNMChZw9LTZK7BA%40mail.gmail.com.
