#44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro

Type Theory Forall

• Episode: #44 Theorem Prover Foundations, Lean4Lean, Metamath - Mario Carneiro
• Website: Type Theory Forall
• Feed URL: https://www.typetheoryforall.com/episodes.mp3.rss
• Duration: 02:13:31
• Published: 2024-11-06 22:00

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.

Links

• Lean4Lean github
• Metamath
• Metamath0
• Lean Foundations Discussion
• Large Elimination / Singleton Elimination