Zulip Chat Archive

Stream: Lean Together 2021

Topic: MM0/MM1 talk

Mario Carneiro (Jan 04 2021 at 20:58):

Just a reminder that my talk MM1: A Lean-style proof assistant for Metamath Zero (tutorial) is an out-of-band youtube talk; the Q&A session is tomorrow but you won't have time to watch it between the other sessions, so if you are interested you should watch it some time tonight

Rob Lewis (Jan 05 2021 at 09:12):

Watching this now -- it's a really nice demo, thanks Mario!

Rob Lewis (Jan 05 2021 at 16:05):

And a reminder that you should track down Mario at the upcoming social session to ask him about this!

Last updated: Dec 20 2023 at 11:08 UTC