alt Hacker NewsNote that paper is saying that the lean proof and the natural language proof do not necessarily coincide. It is not saying that the lean proof is wrong, just that the lean proof does not necessarily mean the natural language proof is correct.
Replies
macleginn • yesterday at 9:17 PM
The thing is, you often see people saying, ‘They have a Lean cert, so it has to be correct, even if I don't understand it.’
A lean proof and a paper proof can diverge. But the statements have to correspond. I think that is what "mistranslated" means here.