Thanks for the link and the TOC ! On Saturday, January 8, 2022 at 2:57:55 PM UTC+1 savask wrote:
> > 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/6d6d1dcd-3dfa-4168-9b8f-649a8bd98891n%40googlegroups.com.
