> formalizing something like FLT is currently completely unfeasible.

No, Kevin Buzzard is leading a project to formalise FLT for a couple of years now. Anthropic scooped him last month, but his project involves more than just producing a formal proof: https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-h...