alt Hacker NewsA lean proof and a paper proof can diverge. But the statements have to correspond. I think that is what "mistranslated" means here.
A lean proof and a paper proof can diverge. But the statements have to correspond. I think that is what "mistranslated" means here.
But the "mistranslation" is of the procedure that arrives at the final statement. The final statement, the thing that the lean code proves, itself has been well vetted by humans. So the lean proof correctly proves the NS blowup, it's just that the natural language paper has some mistakes and doesn't exactly follow the route the lean proof takes.