Conversation between Stephen Wolfram, Norman Megill and Mario Carneiro

[savask]

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.

[Benoit]

Thanks for the link and the TOC !