Think of it this way. A math paper is pseudocode that has never been run. A Lean formalization is a running program. (It really is.)

In the process of formalizing, you find bugs, you find gaps, you find ways to fill those in. Maybe you rewrite part of the proof. Maybe you didn't quite wind up with the same result. Perhaps your theorem has some new conditions or something.

Was the original paper true? Maybe. But that isn't what you verified. What you verified is almost surely true though. So you take the win, and move on.

They mean a different statement, a different theorem. You have to understand that translating a theorem written in English text to lean code is also a non trivial step.

No, prove something else could mean proving something very trivial thus making the proof meaningless on its own.

IE a proof can be true, rigorous, and not at all what was asked for.