It wasn't clear that LLMs were up to a Lean translation task of this scale until now. The background required to formalize the FLT proof was tremendous, so many people assumed we would have to wait until all of that was formalized in Lean before we could ask it to formalize Wiles' proof. Now it seems like almost any mathematics paper we can ask an LLM to formalize, including all necessary background, and it can just do it.