Interactive Theorem Proving in Education and Research

24 July 2024 // University of Exeter // Online

A one-day workshop focused on how interactive theorem provers, like Lean and Isabelle, can be used in mathematics and computer science. This event is ideal for educators and researchers who use deductive proof.

No prior experience is necessary: the day starts and ends with hands-on sessions that provide practical experience for those unfamiliar with Lean.

Sponsored by the University of Exeter Education Incubator.

Invited speakers

  • Jeremy Avigad (Carnegie-Melon University)
  • Achim Brucker (University of Exeter)
  • Kevin Buzzard (Imperial College London)
  • Heather Macbeth (Fordham University)
  • Diego Marmsoler (University of Exeter)
  • Patrick Massot (Universit√© Paris-Saclay)
  • Athina Thoma (University of Southampton)