This is quite useless actually. The whole point of formalizing FLT was to clean up modern number theory into reusable abstractions that prove it.
If its 13 million LoC, it might involve so much spaghetti that its unusable other than the result
physics is like sex: sure, it may give some practical results, but that's not why we do it
physics is like sex: sure, it may give some practical results, but that's not why we do it