Great talk, and I hope it gets a wider audience. I have to confess to some envy, as you're accomplishing a great deal of what I set out to do with Ghilbert and stalled out on.
A question: when translating to Lean, do you have to depend on classical logic (ie "open classical"), or are you somehow able to avoid that? If I get some time (a bit rare these days) I would like to play with it in more detail. Raph On Wed, Jul 29, 2020 at 10:11 AM Mario Carneiro <[email protected]> wrote: > For those who might be interested, I just presented MM0 at the CICM > conference, and the video is now on youtube: > > https://youtu.be/CxS0ONDfWJg > > (It occurs to me that I should have announced this *before* the talk, in > case folks were interested in registering for free in order to attend > directly. You can still ask questions here if you want.) > > 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/CAFXXJSt_99WS9eusOuNv9iL%2BF665_APRLJQ9jVUqXzxer1GCZA%40mail.gmail.com > <https://groups.google.com/d/msgid/metamath/CAFXXJSt_99WS9eusOuNv9iL%2BF665_APRLJQ9jVUqXzxer1GCZA%40mail.gmail.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/CADBEgNM6WD4rYwrFqJQ1sE5z%3DL%2BZAy2b7h5jyEqd0%2Bug%2BSaoeQ%40mail.gmail.com.
