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 <[email protected]> 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/f22c9d81-ec51-4337-aa8f-2884e7cf1e58n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/f22c9d81-ec51-4337-aa8f-2884e7cf1e58n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSvRB%3DnqcZp1xc7f8MMd%2Bf14FwNjVVQK%3DLBLaZGkCBZAmg%40mail.gmail.com.
