Have you heard about the lambda-calculus, dependent types, intuitionistic v.s. classical logic, or the Curry-Howard correspondence?
During this talk you will learn much about these, but not presented in the usual academic way... No! Clojure and Emacs/Cider will serve as learning vehicles, throughout a gently-paced live-coding Mathematics session !
For this we will use LaTTe, an open source proof assistant library for Clojure, probably one of the most addictive single-player puzzle game ever!
NB: no greek letters were harmed during the preparation of this talk.