Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
Claim. Write and, for a set , for the property asked by Problem 598: there is a coloring such that every contains countable subsets of all colors; for a cardinal this is , equivalently . Theorem 4.3 of the note: assuming suitable large-cardinal hypotheses, there is a forcing extension in which , so , and there is a cardinal with such that holds exactly for the cardinals . In that model the coloring fails for every , so a positive answer for every infinite , the reading of Erdős's Problem 8 recorded on the problem page, is not a theorem of ZFC if ZFC with those hypotheses is consistent.
Submission note. Posted to the site's forum by Przemek Chojecki on 22 April 2026:
GPT-5.4 Pro came up with a nice argument involving Magidor cardinals to get yes/no classification, it does however need to assume certain large cardinals hypotheses, making it still open in ZFC. Here's a note and here's its formalization in Lean by Aristotle.
Covers. The not provable side of the question, as a consistency statement relative to the large-cardinal hypotheses the note takes from Garti and Hayut: in the note's model the coloring fails for every , so ZFC does not prove a positive answer for every infinite . That side alone leaves the question open. The ZFC instances that the note also proves are recorded on the problem page.
Hypothesis. The note does not name the large-cardinal hypotheses; it takes them from Claim 1.10(a) of S. Garti and Y. Hayut, The first omitting cardinal for Magidority, Math. Log. Q. 65 (2019), no. 1, 95–104 (library card), which gives a forcing extension with a Magidor cardinal whose first omitting cardinal is ; the note's Theorem 4.1, a bounded-set obstruction, and its Corollary 4.2 then give , and its Theorem 3.1 places the least failing cardinal above with cofinality above . The result is a relative consistency statement and settles nothing in ZFC; the note's Remark 4.4 says so.
Also in the note. Proposition 2.1 proves for every regular uncountable , the repaired form of the stationary-set argument of thread post 4782 (the coloring there was defined only on countable sets whose supremum has cofinality ; any default color on the others repairs it). Corollary 2.8 extends this to every by a countable-product theorem; since for by Hausdorff's formula, this is the case and no more, and below the property holds vacuously. These ZFC results decide the instances positively; the problem page records them.
Source. "A Threshold Consistency Theorem for Erdős Problem 598", a note dated April 2026 with no author line, posted on the site's discussion thread on 2026-04-22 (post 5699) by Przemek Chojecki, who writes that GPT-5.4 Pro developed the argument. The claimant is Chojecki, who published it, with the system named as the post names it. Not refereed, not on arXiv.
Formalization. The post links a Lean 4 file, which it credits to
Aristotle and whose header declares it a formalization of the note. The
file proves the closure theorems (thick/thin sums, countable products),
parts of Theorem 3.1 and the bounded obstruction of Theorem 4.1; it leaves
Solovay's partition theorem, and with it Proposition 2.1, and the
Garti–Hayut inputs as sorry; and it states Theorem 4.3 as
theorem threshold_model_description : True := trivial, so the threshold
model is not formalized at all, as thread post 6747 (2026-05-30) reported.
Post 5709 (2026-04-22) reported citation errors and slight mismatches
between the assumed statements and the literature. The file was not built
or audited here, so the page lists no formalized evidence.
Standing. No reviewer is recorded and the site labels the problem OPEN
with no verdict, so the claim stays claimed. A later posting,
Wu's answer of
2026-05-24, reaches independence from ZFC relative to the rank-into-rank
axiom I1 by a different route, and
White's report of
2026-07-28 reproves that independence.