Comment by Azantys

The whole point was for the formalization to be clean enough so it could be reused in other parts of mathematics as I understand it. 13M lines of AI slop which have never been checked do not sound like what the original goal for such a formalization was. Also Claude didnt prove anything it just translated an already existing proof by Wiles into Lean, so it didn't actually contribute anything other than "Guys we did this thing, look how great our model is!". We never questioned that a printer can print faster than a human can write, but we dont let printers write novels.