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.