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.
