Hmm, two thoughts: 1. If reading is more your thing than video, you can get some idea of what this is about from https://github.com/geohot/twitchcoq
2. Do videos on formal proofs, whether coq or Isabelle or lean or (fill in the blank), whether positive or negative, ever get 14,000 views? Sounds like a lot for a topic which is still off the beaten path for a lot of people. On December 21, 2019 6:13:50 PM MST, Glauco <[email protected]> wrote: >I was googling for a video about Emetamath, Thierry's plugin, but I >found >this recent video, that caught my attention: > >https://www.youtube.com/watch?v=hKi9Q3S1Nsg > >The title is "George Hotz | Programming | twitchcoq : pt 3, mostly I >want >to complain about metamath" > >I'm having a late night "dinner", so I've not had time to understand >the >whole story yet, but it looks like George (a well-known hacker, you can > >read about his life on Wikipedia) has streamed and recorded a number of > >multi hours videos (this is the third one) about him programming a >parser >for Metamath (he read the Metamath book just before the videos). > >I've had time to look at the first few minutes, where he complains >about >set.mm > > >Glauco > >-- >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/c8167c6f-7c78-4764-87fa-aa1dba262f58%40googlegroups.com. -- 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/A0DFD28A-92B4-4938-A9B1-5B947E0B221A%40panix.com.
