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 formal

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 https://adam.math.hhu.de/#/g/leanprover-community/nng4