You only have to prove the formalization of the theorem statement. The formalized statement is guaranteed to be true if Lean says so.

There will always be a leap from the real world to the formal world.