Proved; the site's label is PROVED (LEAN). Lorentz's Theorem 1 [Lo54] gives every infinite $A$ a density-zero complement with $A+B$ cofinite; the Lean qualification of the site's label corresponds to the proof the formal-conjectures catalog links, a third party's Lean proof. The claim page Lorentz's sparse additive complement records the acceptance evidence, the refereed publication and the catalog's curator, Thomas Bloom; the Lean proof carries no formal-verification credit in this corpus.