The Heilbronn Institute is delighted to be supporting a visit by Professor Emily Riehl from Johns Hopkins University to give the next Heilbronn Colloquium on 3 July 2025 at University College London. The London Heilbronn Colloquia are a series of triannunal lectures by distinguished mathematicians and theoretical physicists at the forefront of current research. They are aimed at a general mathematical audience and informal interaction with the speaker is invited.

A Reintroduction to Proofs

Emily Riehl, Kelly Miller Professor of Mathematics, Johns Hopkins University

3 July 2025 | time to be confirmed

Venue: Department of Mathematics, University College London, UK

An introduction to proofs course aims to teach how to write proofs informally in the language of set theory and classical logic. In this talk, I’ll explore the alternate possibility of learning instead 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, there is an opportunity to practice writing proofs in this formal system by interacting with computer proof assistants such as Rocq or Lean. Equally, intuitions built from an early informal introduction to dependent type theory will make it easier for those who aspire to write computer formalized proofs later on.

---

Information on past and future colloquia is available here

Join the Heilbronn Event mailing list to keep up to date with our upcoming events