PROVED (LEAN). The site labels the problem PROVED (LEAN) (page last edited 19 October 2025; accessed 2026-09-04 and 2026-10-07) and credits Chen and Ruzsa [ChRu99] with the proof of the stronger conjecture that every infinite subseries over squarefree numbers is irrational; the frontmatter standing derives from the claim page (Chen–Ruzsa, 1999) for that refereed paper. The Lean qualifier is a third-party formalization of the paper's argument that formal-conjectures cites, described under Formalization; this corpus has not built or audited it.