If you’re interested, here are some really fun games/puzzles to learn the basics of Lean: https://adam.math.hhu.de/