Abstract: Since computers were invented, mathematicians do not have to spend hours doing computations, and can use their time to write proofs- which they need to check and double-check. What if they could also use computers to help with this? They would have more time to drink coffee! Lean is a functional programming language that allows you to write theorems and proofs, and it verifies whether they are correct. In this session, we will have fun learning the basics about Lean while playing a game! Please, bring your own computer (you don’t need to install anything).