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!