I dreaded reading this but it is actually a pretty lucid post by Kevin Buzzard. I wish him luck in his efforts to develop a more useful formalization of FLT. I also agree with Kevin that the question of whether a body of mathematics is fundamentally valid (or, like 1930s Italian geometry needs to be rebuilt from the ground up) is one of the areas where, even in the absence of mathematical insight, costly "yes/no" answers like this can provide a useful supplement to the mathematical community's consensus.
I think that many of us had argued for funding our work by appealing to the possibility that everything is "wrong" and we need to be more rigorous, etc., and i believe that AI does obviate that use case. this was, honestly, never the reason that any of us were interested in proof assistants, but it was something legible that we could explain to funding bodies and the public. now we need to find a way to explain to those people why we are doing what we are doing, and i think it would be good if our explanation were more truthful this time.
FLT: Anthropic has beaten me to it (one of their internal models, using the prove2.me platform, has formalized a complete proof of Fermat’s Last Theorem (FLT) in Lean). ~ Kevin Buzzard. https://xenaproject.wordpress.com/2026/09/04/flt-anthropic-has-beaten-me-to-it/ #AI4Math #LeanProver #ITP