Yes, you need to manually verify the statement of the theorem of interest of formalized correctly. But you don't need to anything more than this: you can rely on the proof being correct. And the proof is overwhelmingly the most amount of code.

>you don't need to anything more than this

You also have to check for things like sorry or defining axioms.