Logo

Type Theory Forall

Type Theory much beyond inference rules

Episode image

#33 Z3 and Lean, the Spiritual Journey

Leo de Moura

Apr 11th 2024   |  125 min
0:00
0:00

Not satisfied with implementing one of the most popular automated theorem provers, Z3, Leo de Moura also tackles another extremely hard problem in our field and implements a brand new interactive theorem prover from scratch, Lean. In this episode we dive into the mind and philosophy of this man.

Links

Sponsors

join our discord