If you want to get an idea of what proving things in Lean is like you could try this super fun game, which I think is by one of the people behind the FLT formalization project:

https://adam.math.hhu.de/#/g/leanprover-community/nng4