Interactive Theorem Proving in Lean I

In this mini-course, we explore the world of proof assistants and learn how to encode mathematics on a computer using Lean. The goal is to help participants develop new programming skills while becoming acquainted with formal mathematics. Each session will combine a lecture with hands-on computer practice. Practice files for each session will be provided and no prior installation of Lean is required.