The attendees of the tutorial on interactive theorem proving in Lean by Floris van Doorn (7th, 8th June) are kindly asked to bring their own laptops for an active participation in the session.