A proof was recently formalized in the Lean proof assistant by Anthropic, leaving little doubt that Fermat's Last Theorem is indeed a theorem. There was (and still is) ongoing work by mathematicians to formalize a more modern proof in Lean in a more handcrafted fashion, but they were robbed of some of the joy of that activity by the AI companies, which seems will be a repeating pattern going forward.