Undergraduate Talk on Lean4 and the Curry-Howard Isomorphism

Stream: general

[Luis Wirth]

Hi everyone!
I recently gave a 45-minute talk at ZUCCMAP (Zurich Undergraduate Colloquium in Computational Science, Mathematics, and Physics) at ETH Zurich, introducing Lean4. The talk covers type theory, lambda calculus, and the Curry-Howard Isomorphism, with comparisons to C++ to make it accessible for undergraduates.

You can watch it on YouTube.
I'd love to hear your feedback! :)