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