but i don't understand... isn't Wiles's proof and its numerous rewritings already in the training set?

Yes. The point was not coming up with the proof from scratch. The point was writing it all down in Lean to make it fully machine checkable.

Of course it is. The interesting thing is that it was able to produce a Lean proof in 11 days, when there's been an ongoing project for several years to do the same thing (though a somewhat different proof) that is nowhere near done.