PROVED (LEAN). The site labels the problem PROVED (LEAN) (page last edited 28 October 2025) and credits Frankl and Lin, independently, with the finiteness, the largest solution being $2^7=2!+3!+5!$; Lin's memorandum is recorded on its claim page (Lin, 1976). The Lean qualifier refers to a classification of all solutions produced by the AxiomProver system in June 2026, which names no informal source and is a pending claim on its own page; this corpus has not built it. There is no refereed write-up. The standing in the frontmatter derives from the claim pages.