This talk will unravel the relationship between computer programs and mathematical proofs. The first half will build up the mathematical machinery and historical context to explain the conceptual bridge that connects programs and proofs [the Curry-Howard Isomorphism]. The second part will explore the potential implications of (computer) proof assistants on the mathematical community and propound the idea that students, educators, and researchers alike might benefit from this emerging paradigm.
There will be a tea before the talk (@ 4:00 PM), and pizza after (@ 5:30 PM).