DISPROVED (LEAN). The site labels the problem DISPROVED (LEAN) (page last edited 12 January 2026) and credits Neel Somani, working with ChatGPT, with an explicit infinite family of solutions, recorded on its claim page (Somani, 2026); the Lean qualifier refers to an Aristotle-generated formalization of that family, which this corpus has not built. The preprint of Feng and coauthors (29 January 2026) reports the same family, found by their Gemini-based agent Aletheia in December 2025, as a pending claim on its own page. There is no refereed write-up. The standing in the frontmatter derives from the claim pages.