---

Claim. Granted Baumgartner's relation $\omega_1^2\not\to(\omega_1\omega,K_{\aleph_0,\aleph_0})^2$, there is a connected bipartite graph $F$ on exactly $\aleph_1$ vertices, of diameter at most $3$, containing no $K_{\aleph_0,\aleph_0}$ (and no $K_4$, being bipartite), with $\omega_1^2\not\to(\omega_1\omega,F)^2$. The coloring that witnesses Baumgartner's relation, with blue graph $H$, has no red set of order type $\omega_1\omega$; a theorem of Shelah (Claim 3.4(2) of Saharon Shelah, Universality among graphs omitting a complete bipartite graph, Combinatorica 32 (2012), no. 3, 325-362, doi:10.1007/s00493-012-2033-4, as the manuscript's reference list gives it, applied with $\lambda=\aleph_1$ and $\kappa=\theta=\aleph_0$) gives a bipartite $K_{\aleph_0,\aleph_0}$-free graph $F$ on $\aleph_1$ vertices that does not embed into $H$, so the same coloring has no blue copy of $F$ either. The first question of Problem 597 therefore has a negative answer: not every $K_4$-free, $K_{\aleph_0,\aleph_0}$-free graph on at most $\aleph_1$ vertices satisfies the relation. The manuscript is Alex Chengyu Li, "A Nonuniversality Obstruction to an Ordinal Graph Partition Relation", version 1.1 of 2026-09-09, a Zenodo deposit under a Creative Commons Attribution 4.0 license (doi:10.5281/zenodo.22671916); it is not held, and this page states it from its record, its statements, its reference list and the claim's summary.

Submission note. Posted to erdosproblems.com as a proof claim by Alex Chengyu Li (account alexchengyuli) on 9 September 2026, giving "Proof Engine (https://doi.org/10.2139/ssrn.7237460; https://doi.org/10.5281/zenodo.22346064), with GPT-5.6 and GPT-6 Astra." as the AI used:

We obtain a negative answer to the unrestricted part of #597 by combining results of Baumgartner and Shelah. The finite-target question is not settled here. Baumgartner's result, reported by Erdős (1987), p.224, gives a colouring of $\omega_1^2$ with no red set of order type $\omega_1\cdot\omega$ and no blue $K_{\omega,\omega}$. Let $H$ be its blue graph. Shelah's Claim 3.4(2), with $\lambda=\aleph_1$ and $\kappa=\theta=\aleph_0$, gives a bipartite, $K_{\omega,\omega}$-free graph $F$ on $\aleph_1$ vertices that does not embed into $H$. Since $F$ is bipartite, it also has no $K_4$. The same colouring therefore has neither the required red set nor a blue copy of $F$. Our note applies these results to #597, gives a rank proof of the graph step, and formalizes the deduction from Baumgartner's theorem. The basic tree construction for the graph step already appears in Shelah's proof. Notes: The Lean development formalizes the graph constructions and the deduction of the main counterexample from the precise Baumgartner theorem statement. Its sole external theorem input is 'Baumgartner597PairColoringWitness'; the final endpoint is 'erdos597_reference_gated'. The proof of that cited theorem is not included in the codebase: I located Erdős's published report, but have not located a primary text containing Baumgartner's proof. This is the boundary of the machine verification (Reference-Gated). The graph-theoretic argument is proved in the development, so Shelah's theorem is not a second external input.

Covers. The first question, negatively, through one target of size exactly $\aleph_1$. It leaves open whether the relation holds for every countably infinite target of the stated kind, and it does not touch the second question, the relation for finite $G$, which the claimant states is not settled by this work; the site's proof-claims page files the claim as a full claim, but its own text restricts it to the first question.

Hypothesis. The argument takes Baumgartner's relation as an input. The relation is reported, in a parenthetical remark without hypotheses or proof, in Paul Erdős, Some problems on finite and infinite graphs, Logic and Combinatorics, Contemporary Mathematics 65, American Mathematical Society (1987), 223-228, on p. 224, in the unnumbered paragraph following Problem 3 (library card), and the claimant reports finding no primary text containing Baumgartner's proof; the companion Lean development proves only the implication from that relation to the conclusion. The argument gives the negative answer in ZFC if Baumgartner's relation is a ZFC theorem; as recorded, it proves the implication.

Argument, in outline. As the claimant summarizes it, the graph step is a rank argument, a special case of Shelah's nonuniversality theorem, whose basic tree construction already appears in Shelah's proof; the note applies the two results to the problem and formalizes the deduction from Baumgartner's relation. The argument was not reconstructed here.

Standing. The claimant is Alex Chengyu Li, who filed the result on the site's proof-claims page on 2026-09-09 under the forum name alexchengyuli; the claim's entry names the systems Proof Engine, with GPT-5.6 and GPT-6 Astra. The Lean development in the repository crabsatellite/erdos-597-ordinal-biclique, linked at the pinned commit, proves the implication from Baumgartner's relation taken as a hypothesis: the claimant's notes name that hypothesis as the development's sole external input, Baumgartner597PairColoringWitness, and its endpoint as erdos597_reference_gated, with the graph step proved inside the development. It was not built or audited here, so the page lists no formalized evidence. The site shows OPEN with no verdict and no comments; the manuscript is not refereed and no reviewer is recorded, so the claim stays claimed.