If what you mean is the link in the list of verifiers, I updated it: http://us2.metamath.org/other.html#leanmmverify
Norm On Saturday, May 8, 2021 at 7:13:01 PM UTC-4 [email protected] wrote: > 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/f2fa7ec1-7a3d-4e7d-9f65-d152c5124675n%40googlegroups.com.
