On Wed, Nov 25, 2020 at 8:58 AM Glauco <[email protected]> wrote:
> Hi Mario, > > here > https://groups.google.com/g/metamath/c/raGj9fO6U2I/m/2tQseJ3CBwAJ > you show peano.mm1 in VSCode and you write > "The basic idea is that MM1 is a scripting language for assembling MM0 > proofs and statements. It's untrusted, and functions as the IDE for MM0" > > Looking at one of your presentations I've seen you've also completely > translated set.mm to mm0, isn't it? > > Would it be possible, for you, to video-record a session in which you > proof a simple new theorem (starting from the mm0 translation of set.mm) ? > There is actually quite some work before this becomes a really usable workflow. The problem with the translated set.mm is that there are *no* notations. Everything is s-expressions which makes it pretty difficult to read. Most of my MM0 work has been inside peano.mm1, which is a set.mm style axiomatization of peano arithmetic with all the niceties that MM0 brings to bear. It wouldn't be so hard to demo a new theorem there as there is a pretty decent library of supporting theorems. Alternatively, I could use set.mm0, which is a kind of half baked hand translation of the set.mm axioms into MM0, including notations. I never finished the proof of set.mm1 because I needed a library of basic logic, but I could probably port the peano.mm1 library at this point (since the first part of peano.mm1, on basic logic, would be the same as set.mm). More long term solutions for supporting set.mm would include auto-translating most notations into MM0 style, identifying the constructions that need some new notation, and making some hard decisions for those. MM0 has the requirement that every notation uses a distinct initial constant (or for infix notations, the first constant after the initial variable should be distinctive), which means that a lot of mixfix notations from set.mm like F : A --> B are probably not going to survive. > No audio is needed, and there's no need to make the video available on > youtube to everybody. Just a short session to show us how it would be the > workflow: > load available axioms/definitions/terms/theorems > create new theorem> > write/verify proof > save created proof (add to the pre-existing "stuff") > Especially if you mean the end to end MM workflow, a lot of this is still very much a dream/plan/roadmap and not a current reality. What I can show you now with mm0-rs is the use of MM1 to construct a .mmb binary proof file that can be verified by external MM0 verifiers like mm0-c. I can probably declare a few notations and do the same thing starting from set.mm.mm0, but the result will still be an MM0 proof, not an MM proof. That's what the plan is all about. Mario -- 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/CAFXXJSvB%3DFoinb-06k-tutL0GNw0%3DGo4nwqHvgvfdrV2BOVQUQ%40mail.gmail.com.
