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"

	▲	baq 5 hours ago \| parent \| next [-]
		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!
	▲	emil-lp 5 hours ago \| parent \| prev [-]
		Well, to be fair, with Lean proofs, that's the only thing there is (unless I'm missing something).