Here is the Clay Mathematics Institute DVD of the musical on YouTube.

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.

https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/