Lean is a proof assistant and functional programming language. It is used widely in mathematics to write and verify proofs. The workshop will give a short enough intro that we can play Lean games together that give an easy introduction to the Lean theorem solver. If you want to write proofs but are too lazy to check them, give Lean a try! Also, the games are cool: https://adam.math.hhu.de/#