---

Claim. For every simple graph $G$ with $\chi(G)=\aleph_1$, whatever the cardinality of its vertex set,

$$\forall K>0\ \exists N\ \forall n\ge N:\qquad h_G(n)>Kn,$$

so $h_G(n)/n\to\infty$. Here $h_G(n)$ is the least bound in the Statement of Problem 111, the largest number of edge deletions that an $n$-vertex subgraph of $G$ needs to become bipartite; every admissible bound is at least this one. The threshold $N$ may depend on $G$ and $K$. The second question of the Statement therefore has a positive answer.

The proof goes through a countable-coloring theorem: for every finite $C\ge0$, every graph each of whose finite subgraphs $F$ can be made bipartite by deleting at most $C|V(F)|$ edges has countable chromatic number, at every vertex cardinality, singular cardinals included. Deleting countably many vertices from a graph of chromatic number $\aleph_1$ leaves chromatic number $\aleph_1$, so the theorem yields $\aleph_1$ pairwise vertex-disjoint finite subgraphs $F$ each needing more than $2K|V(F)|$ deletions. One isomorphism type recurs uncountably often, and packing its copies gives $h_G(n)>Kn$ for every large $n$.

On the first question, the behaviour of $h_G(n)$: for every nondecreasing unbounded $g:\mathbb N\to\mathbb N$ there is a graph $G$ with $|V(G)|=2^{\aleph_1}$, $\chi(G)=\aleph_1$ and

$$h_G(n)\le(n-1)\,g(n)\qquad(n\ge1),$$

and under $\diamondsuit$ there is such a graph with $|V(G)|=\aleph_1$. With $g(n)=\lceil\log_2(n+1)\rceil$, one graph of chromatic number $\aleph_1$ has $h_G(n)\ll n^{1+\varepsilon}$ for every $\varepsilon>0$. This confirms in ZFC the conjecture of Erdős, recorded in the remarks on erdosproblems.com, that the Erdős–Hajnal–Szemerédi bound $h_G(n)\ll n^{3/2}$ can be improved to $\ll n^{1+\varepsilon}$ for every $\varepsilon>0$.

Submission note. The Palomar registry's description of entry PALOMAR-2026-10-19-000007, registered on 19 October 2026 by a maintainer of the repository, whose formalization.yaml names Jacob Parish and Andrew Turner as its responsible maintainers:

A Lean proof that for every real C, a graph whose finite subgraphs on m vertices can each be made bipartite by deleting at most Cm edges has countable chromatic number. Hence h_G(n)/n → ∞ for every graph G that is not countably colorable, in particular for every graph of chromatic number ℵ₁. This answers the second question of Erdős Problem 111 in the affirmative.

Covers. The definite question of Problem 111, whether $h_G(n)/n\to\infty$ for every graph $G$ of chromatic number $\aleph_1$: answered yes, as a limit over all sufficiently large $n$ rather than along a subsequence, for graphs of every vertex cardinality. The first question, the behaviour of $h_G(n)$, is open-ended and not a part. On it the claim supplies only the upper bounds stated above. It determines no rate of divergence and no exact order of $h_G(n)$ for any particular graph, and asserts no optimality of the bound $(n-1)g(n)$.

Credit. The countable-coloring theorem, its layered-measure proof and the reading of the upper bound are Plasma AI's. Section 2 of the Erdős Problem a Day report on Problem 111 (https://www.erdosproblemaday.com/report/111, dated 26 July 2026) also proves the reduction of the limit to a finite-density statement; the argument here does not rely on it. The graph of the upper bound is the one built in Chris Lambie-Hanson's ZFC proof of Theorem A of On the growth rate of chromatic numbers of finite subgraphs (Adv. Math. 369, 2020), and under $\diamondsuit$ the Hajnal–Máté graph of his Theorem B. The bound is read off the edge labelling of his Claim 4.1; his construction uses the odd girth of Specker graphs and Shelah's club-guessing theorem as that paper cites them.

Standing. Tier 1. The whole-conclusion independent examination of 2026-10-17 and its separate passing grade find refutation-failed, first for the countable-coloring theorem at every vertex cardinality and then for the full limit. The verification record retains the exact subject, the independent derivations and the findings on the disclosed exposures. That examination is noncomputational. Its classical inputs, among them elementary submodels, compactness of products of finite spaces, the Riesz representation theorem and finite-dimensional convex separation, were checked in their stated forms; their original proofs were not examined. The upper bound and its consequence stated above are tier 1 by a separate independent examination of 2026-10-16 and its separate passing grade, which check Lambie-Hanson's construction at the interfaces listed there; the Specker odd-girth and club-guessing theorems remain external premises. The Lean formalization below covers the limit and the countable-coloring theorem, not the upper bound. It lies outside this repository's Lean closure, so it confers no tier.

Formalization. The repository plasma-ai/erdos-111, at commit de72caf, formalizes the claim in Lean 4 (v4.35.0-rc3, Mathlib v4.35.0-rc3). Challenge.lean states it as Erdos111.erdos_111, for every graph whose least color cardinal chromaticCardinal G is $\aleph_1$, with h G n the largest number of deletions an $n$-vertex subgraph needs to become bipartite; it also states the countable-coloring theorem, Erdos111.countably_colorable_of_linear, and the limit for every graph with no coloring by $\mathbb N$, Erdos111.tendsto_of_not_countably_colorable. Solution.lean proves the three, and comparator.json permits only propext, Quot.sound and Classical.choice. The proof follows the repository's blueprint, which reorganizes the reviewed argument: closure over a set in place of elementary submodels, a chain that starts from the empty set, and limits of laws along an ultrafilter in place of weak-star compactness. The repository's formalization.yaml names Jacob Parish as the formalization's author, records that it was written with Claude Code, and gives its review status as self-assessed, with a Comparator check run on macOS without Comparator's sandbox. The repository's README credits the proof to two models working in alternating steps, GPT-6 Astra in Codex and Claude Opus 5.5 in Claude Code, and the Lean to Claude Opus 5.5 in Claude Code. The repository is registered on the Palomar registry as PALOMAR-2026-10-19-000007, version 1, first registered on 19 October 2026 (the record link; trust level high, automated review outcome neutral), and the entry pins commit de72caf. The source card plasma_ai_2026_bipartizing_finite_subgraphs_uncountably_chromatic_graphs digests it.

Acceptance. Formalized. This corpus rebuilt the formalization, held as the repository's tree at de72caf, at its own pinned toolchain, leanprover/lean4:v4.35.0-rc3 with Mathlib at v4.35.0-rc3, in a sandbox with no network. Comparator, run before anything else built the solution, accepted the three theorems against Challenge.lean. The kernel then replayed, from an empty environment, every declaration each of the three depends on, and accepted them all. Each theorem's type, and every constant its statement reaches, are identical in Challenge.lean and Solution.lean, and each depends only on propext, Classical.choice and Quot.sound (the replay receipt, 2026-10-19). The graded fresh-context review of the statements, by a reviewer and a distinct grader, both Claude Opus 5.5 agents working from fresh contexts, found all three faithful, erdos_111 covering the second question whole. Acceptance rests on the replay and that review, and covers the limit, the definite question. The open-ended first question is not a part, and the upper bound stated above is not formalized; it keeps its tier-1 standing. The formalization's own Comparator run is reported, not counted.

Depends on. The countable-coloring lead (tier 1), with its layered-measure proof of the countable-coloring theorem and its Proposition B for the upper bound. No native claim card is a premise. The upper bound also uses the construction of Lambie-Hanson's Theorem A, credited above.