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.’
They are right? The lean proof is correct. It's the natural language proof that potentially isn't (or at least it isn't identically structured to the lean proof)
They are right? The lean proof is correct. It's the natural language proof that potentially isn't (or at least it isn't identically structured to the lean proof)