Interactive Theorem Proving in Education and Research

24 July 2024 // University of Exeter // Online


The day consists of six talks on education and research using Lean and Isabelle.


The workshops serve as an introduction to mathematical proof using Lean. We will use both:

The natural number game is a good introduction to the syntax of Lean and is ideal if you have no prior Lean experience. It requires no more than a web browser.

Mathematics in Lean shows you how to work seriously with Lean, introducing mathematical objects such as: functions, groups, and rings, metric and topological spaces

Please bring an Internet-enabled laptop if you wish to participate in the workshops in person.

For ‘Mathematics in Lean’, it will make things run more smoothly if you sign up for a GitHub account before arrival. Then follow the instructions in the Mathematics in Lean GitHub repository to either install locally or (recommended for new users) run in GitHub Codespaces.


Registered participants can join in-person or via Zoom. A Zoom link will be emailed to all participants.

In-person sessions take place in the Digital Maker Space, in Level -1 of the Forum Library.

Digital Maker Space
Forum Building
University of Exeter
United Kingdom


If you have any questions, please email Gihan Marasingha. The organisers are

  • Gihan Marasingha
  • Barrie Cooper
  • Taro Fujita