Proved. The catalog labels the problem PROVED (LEAN) (page last edited 28 May 2026), saying the proof was verified in Lean and crediting Chojecki and GPT-5.4 Pro via Tao--Teräväinen [TaTe25]; the label is retained from the catalog, and the frontmatter standing derives from the claim page (Chojecki, 2026) for Chojecki's deduction, accepted on the curator's credit and on Tao and Teräväinen's adoption of the deduction as Remark 1.4 of their preprint. The status-defining source is arXiv:2512.01739v2, Remark 1.4, physical p. 5, a preprint; the Lean qualifier rests on a formalization of the deduction that assumes the Tao--Teräväinen theorem as an axiom, described under Formalization, and is not independent verification of the input. An accepted partial claim page records Erdős and Straus's 1971 cases, the monotone sequences and the sequences growing past a power of $\log n$.