3 ms·
I see. It still feels like a bit of an oddly solemn way of saying "this is the part we admit responsibility for"
by danielrmay 2mo ago
I see. It still feels like a bit of an oddly solemn way of saying "this is the part we admit responsibility for"
- emil-lp 2mo agoWell, to be fair, with Lean proofs, that's the only thing there is (unless I'm missing something).
- baq 2mo agoIt’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!
- jhanschoo 2mo agoTraditionally, 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.