Most of the work in formalization is domain modeling and API design. Given the wide range of concepts that Wiles' proof depends on, I doubt that such a project will be done any time soon.

In a discussion on the Lean forum, Kevin Buzzard seemed pretty pessimistic. Seeing as he would probably be best suited to know the challenges of formalizing FLT, I'm adjusting downward.

@BoltonBailey Does this take into account the trajectory of AI assistants? Perhaps it would be more trivial to formalize such a proof later than it is now?

@wadimiusz Hard to say, Kevin is often ready in his writings to admit that neural networks aren't his area of expertise. My take is that if you think AI will be really powerful by 2029 and able to either read papers or make arguments itself, you might think this is likely, but if you were expecting humans to do most of the work, it seems much less likely.

@BoltonBailey In case anyone's wondering why I bet yes. One might see the problem of automatically searching formal proofs for a given theorem as a problem where verifying a suggested candidate is trivial, but proposing a good candidate is damn hard, right? And it makes sense, I guess, to use AIs as good suggestors - even modern LMs, which can generate good ideas sometimes and rubbish at other times; because we already have a nice verifier, we just can't bruteforce all the candidates when the hypothesis space is so huge. That's why I am guessing that finding formalized proofs will be much easier as AI capabilities skyrocket. Let us see in 2029 how off my model is.