Workshop on Mathematical Proof Assistants

Steven Kelk (FSE, DACS) opened the event with a short introduction. Johan Commelin from Utrecht University joined online to speak about human–computer collaborations in mathematics and the development of the Lean theorem prover. Pieter Collins (FSE, DACS) gave a hands-on tutorial introducing the basics of Lean and its underlying ideas. It was great to see many students participating, and actively joining the tutorials and discussions. The program concluded with interactive theorem-proving games and informal discussion over drinks and snacks.