---

Claim. Write $\mathrm{E623}$ for the positive answer to Problem 623: every $f$ from the finite subsets of a set $X$ of size $\aleph_\omega$ to $X$ with $f(A)\notin A$ has an infinite independent set. The claim is that $\mathrm{E623}$ is independent of ZFC, with the two sides of different strength: ZFC $+\,\mathrm{E623}$ is consistent if and only if ZFC plus a measurable cardinal is consistent, and ZFC $+\,\neg\mathrm{E623}$ is consistent if and only if ZFC is. The route is a chain of equivalences proved in ZFC, $\mathrm{E623}\Leftrightarrow\mathrm{FS}1(\aleph\omega,\omega) \Leftrightarrow\mathrm{FS}\omega(\aleph\omega,\omega) \Leftrightarrow\mathrm{Fr}\omega(\aleph\omega,\omega)$, from the problem through free-set properties for maps with singleton and then countable forbidden sets to Koepke's free-subset property for structures with countably many symbols; Koepke's 1984 theorem, on the corpus's card of the paper, then supplies both consistency statements. The result, its labeled propositions and the corpus's account of the manuscript are on the card of the preprint. The claimed outcome matches Erdős's own suggestion, recorded in the site's commentary, that the $\aleph_\omega$ case might be undecidable. The argument was not reconstructed here.

Standing. The claimant is Sungchul Lee, who posted the result in the site's discussion thread on 2026-06-04 and names GPT-5.5 Pro as the system used. The written form is a six-page manuscript dated 2026-06-04 in the claimant's repository; the repository also holds a Lean 4 development, added 2026-06-05, whose README describes it as a formalization of the bridge $\mathrm{E623}\Leftrightarrow\mathrm{FS}1\Leftrightarrow\mathrm{FS}\omega \Leftrightarrow\mathrm{Fr}_\omega$ (theorem Erdos623.zfcBridge, stated for any infinite well-ordered type) and not of the consistency statements. In the thread, Nat Sothanaphan reported on 2026-06-04 that a standard verification check found no issue and that the result would count as a full solution, Johan Land agreed on 2026-07-25, and Elliot Glazer seconded on 2026-08-16, without having checked the details, and recommended labeling the problem independent. Those are thread endorsements, not an acceptance: the site's curator has not changed the label from OPEN or credited the result, there is no refereed publication, and nothing was built or audited here. The claim therefore stays claimed. A later partial claim covering the measurable-cardinal half, which its author describes as independent of this one, has its own page, Crawford's consistency proof.