I don't think the truth of the theorem is ever in doubt so any attack would be silly. But the proof would enable tutorials like this: https://github.com/htzh/flt_for_human/blob/main/math/001-fre...
which would be hard to do without a proof outline as agents are not good at math per se, even though they are very knowledgeable and capable.
I don't dispute the truth of the theorem (since I possess my own proof of it, much more concise than the putative Lean or Wiles proofs, i.e. just a few pages).
The Lean system has already experienced soundness bugs.
The question is, will future generations doublecheck this proof with a frozen Lean system of today? There is a lot of incentive in having LLM's be the first to find high profile theorems like this.
I wouldn't vouch my hand in fire in asserting the validity of this gigantic proof.
Proofs are erasable. If you don't doubt it exists why do you care? Understanding is a side effect. Only people who want to understand the proof would need to care about it.
