On Wed, Jan 15, 2020 at 8:16 AM vvs <vvs...@gmail.com> wrote: > I was very interested in FOMM 2020, but as there is no transcript I'm > forced to look at slides and read some second hand impressions. >
All the talks were recorded and streamed, and they are set to appear on youtube shortly. I'll post a link when they come out. > In case someone missed it and as it's to some extent related to subject: > > "Mario Carneiro talked about metamath 0. I wish I could say more about his > work, but it is too foundational for me to understand it properly. All I > know is that we had a proof of Dirichlet’s theorem on primes in an AP in > metamath and then Mario pressed a button and we had one in Lean, and it had > been written by a computer and was incomprehensible. Scary?" > > That were Kevin Buzzard's impressions :) > I had to skip the demo due to time constraints (or time management issues), so it ended up looking mostly like a theoretical analysis of bootstrapping theorem provers rather than "Mario shows us a weird proof assistant" which was what I was actually going for. Oh well. 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 metamath+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSv43VdGhOarO3i5bbdwTeD3niumUgghW1XqVukDE4QbKw%40mail.gmail.com.
