No, the correctness isn't for the "inside the Lean proofs", but for the translation of "human language math" and its formal Lean variant.
I see. It still feels like a bit of an oddly solemn way of saying "this is the part we admit responsibility for"
Traditionally, a mathematician would be implicitly responsible for all that (if they were to publish Lean code) and also the intellectual work that led to the artifact of the mathematical paper (and code, if part of the contribution). This statement should rather be read as an acknowledgement of limitation of authorship from the implicit, traditional understanding.
Well, to be fair, with Lean proofs, that's the only thing there is (unless I'm missing something).
It’s more than you get from free software - you get no proofs, no warranties and any responsibility of its authors are their pure good will. Reminder lean proofs are software!