Comment by kevinbuzzard

Indeed. I'm not formalising FLT because I think it might be wrong -- I'm formalising it because I know the proof is correct, and using the project as an excuse to get some modern number theory into Lean's mathematics library. My hope is this will increase the chances that systems like Lean will one day be able to help modern mathematicians.