From Computerphile.

Gödel’s Incompleteness Theorem explained with Pen, Paper & Lean (the proof assistant) Professor Thorsten Altenkirch is based at the University of Nottingham.

Computerphile is supported by Jane Street. Learn more about them (and exciting career opportunities) at: https://jane-st.co/computerphile

This video was filmed and edited by Sean Riley.

Computerphile is a sister project to Brady Haran’s Numberphile. More at https://www.bradyharanblog.com