Comment by Azantys
7 hours ago
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.
Then why is the guy not cleaning it up. Clearly he thinks it’s done and he’s moving on to do side things. He also explicitly said it went on to do more than what he was required to do.
Are you hallucinating? Because huge portion of what you wrote directly and logically contradicts the quotation I wrote.