I stumbled upon a recent video conversation between Stephen Wolfram, Norman Megill and Mario Carneiro, and was surprised to find that apparently it wasn't mentioned on the webpages or the google group. Here's the video itself:
https://www.youtube.com/watch?v=zpDvP47Ppjs The video covers a variety of topics, from Wolfram trying to understand the core design principles of Metamath with the help of Mario, to Norman explaining original motivations behind the system. Since the video is two and a half hours long, I prepared some timestamps: 2:45 - Start of the conversation 3:40 - Norm on how Metamath started 6:10 - Schemes 23:50 - Standard logic textbooks vs Metamath 43:10 - Types 57:45 - Other logics in Metamath 1:07:07 - Norm about the goal of Metamath 1:36:30 - Metamath-Zero and applications of formal proofs 2:07:10 - Metamath as a hobby for Norm 2:10:10 - Human-readability of formal proofs 2:13:00 - Wolfram's result on boolean algebras in Metamath 2:14:50 - Proof translation and minimization 2:20:00 - Mizar and other PAs 2:26:20 - Commonalities between proof systems 2:36:30 - Norm's life and Metamath I personally quite enjoyed the conversation, hopefully others will also find it interesting. -- 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/f6f14981-77c8-40ee-9ca6-77be85895da8n%40googlegroups.com.
