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.
#44 Theorem Prover Foundations, Lean4Lean, Metamath
Mario Carneiro
Nov 6th 2024 | 134 min
0:00
0:00
