# PIMS Distinguished Lecture

**
Fri., Feb. 10, 2023 3:30 p.m.
**

**
Location: Live Stream (Zoom)
**

**Speaker:** Emily Riehl, John Hopkins University

**Title:** A Reintroduction to Proofs (72 kB)

**Abstract: **

In an introduction to proofs course, students learn to write proofs informally in the language of set theory and classical logic. In this talk, I'll explore the alternate possibility of teaching students to write proofs informally in the language of dependent type theory. I'll argue that the intuitions suggested by this formal system are closer to the intuitions mathematicians have about their praxis. Furthermore, dependent type theory is the formal system used by many computer proof assistants both "under the hood" to verify the correctness of proofs and in the vernacular language with which they interact with the user. Thus, students could practice writing proofs in this formal system by interacting with computer proof assistants such as Coq and Lean.

**Please pre-register at:** https://uregina-ca.zoom.us/meeting/register/tJYrce6grzstHtPC6-JZKLPzbn_aFukL0I4l

The zoom link for this talk will be provided to you when you register.