Interactive Theorem Proving in Education and Research
24 July 2024 // University of Exeter // Online
Information
The day consists of six talks on education and research using Lean and Isabelle.
Workshops
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.
Participation
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
Streatham Campus
University of Exeter
United Kingdom
EX4 4PZ
Consult the Campus Map to help locate the Forum Library.
Contact
If you have any questions, please email Gihan Marasingha. The organisers are
- Gihan Marasingha
- Barrie Cooper
- Taro Fujita