Mario Carneiro is the creator of Mathlib, Lean4Lean and Metamath0. He is currently doing his Postdoc at Chalmers University working on CakeML. In this episode we talk about foundations of theorem provers, type systems properties, semantics and interoperabilities.

If you enjoy the show please consider supporting us at our ko-fi: https://ko-fi.com/typetheoryforall

Links

• Lean4Lean github
• Metamath
• Metamath0
• Lean Foundations Discussion
• Large Elimination / Singleton Elimination
• Type Theory Forall website
• Type Theory Forall discord