Metamath verifier in Lean 4

[Mario Carneiro]

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

[vvs]

Good news!

This project moves so fast, that some people even expect that it will soon support LSP, apparently. Indeed, the source file is no longer self-contained. I guess that URL announced on Metamath site needs fixing already :)

[Mario Carneiro]

It's still basically in one file, although now that file is https://github.com/digama0/mm-lean4/blob/master/Metamath/Verify.lean . Probably better for the metamath site to point to the repo https://github.com/digama0/mm-lean4/ instead though.

The other file is WIP at the moment, but it now contains some really interesting stuff about a deep embedding of metamath (i.e. appendix C). In particular, I finally managed to prove the theorem that I got stuck on with "metamath in metamath", namely the admissibility of cut. That is, in appendix C there is a definition of the closure of a formal system under applications of axioms; I proved that you can also apply a theorem instead of an axiom. This is of course very important for verifiers, which apply both theorems and axioms when deducing new theorems, even though provability is defined only with respect to applications of axioms. Although now that I think of it I haven't proved anything about the "reduct" operation, which verifiers also rely on...

Mario

On Sat, May 8, 2021 at 6:08 PM vvs <vvs...@gmail.com> wrote:

Good news!

This project moves so fast, that some people even expect that it will soon support LSP, apparently. Indeed, the source file is no longer self-contained. I guess that URL announced on Metamath site needs fixing already :)

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f22c9d81-ec51-4337-aa8f-2884e7cf1e58n%40googlegroups.com.

[Norman Megill]

If what you mean is the link in the list of verifiers, I updated it:

http://us2.metamath.org/other.html#leanmmverify

Norm

[Mario Carneiro]

Could you update the name of the verifier to "mm-lean4"? "Metamath.lean" is a bit generic (file names in lean 4 have to follow some package-oriented naming conventions like in java).

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f2fa7ec1-7a3d-4e7d-9f65-d152c5124675n%40googlegroups.com.

[Norman Megill]

Done.

[vvs]

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.

Benchmarking is a murky business, it pretty much depends on the system. I've got 39.5s (mm-lean4) vs. 18s (canonical metamath). Just for the record, not that I really care. Proving results about MM here is much more important, IMHO.

P.S. Still it would be interesting to compare that with Coq or Agda.

[Benoit]

On Friday, May 7, 2021 at 5:20:47 PM UTC+2 di....@gmail.com wrote:

(and if it is to eventually be verified it is probably best to keep it bare bones)

Isn't it possible to verify only the core of a given program ?

[Mario Carneiro]

On Sun, May 9, 2021 at 10:18 AM vvs <vvs...@gmail.com> wrote:

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.

Benchmarking is a murky business, it pretty much depends on the system. I've got 39.5s (mm-lean4) vs. 18s (canonical metamath). Just for the record, not that I really care. Proving results about MM here is much more important, IMHO.

Actually there was a bug in the original version, it wasn't checking DV conditions correctly. The correct code has more loops in the hottest part of the code, so it impacted performance quite a bit; I currently get about 17 seconds on set.mm (vs 9.8 seconds for metamath.exe), which actually seems pretty close to your numbers if we assume your system just has a lower clock speed than mine.

[Mario Carneiro]

Yes, although you still need the verifier to contain extra state that is ignored for verification purposes. It makes the proofs slightly more cumbersome than they would be with a bare bones verifier but not significantly so. I'm already doing a bit of that in the last few commits, since I want to use the verifier also as a plain parser (rather than the verifier version that consumes all input as soon as it understands it and never produces an actual AST).