Add Erdős Problem 111 (bipartite edge deletion for uncountable chromatic graphs)

[henrykmichalewski]

fixes #341

Formalises Erdős Problem 111: for a graph $G$ with $\chi(G) = \aleph_1$, study the function $h_G(n)$ measuring the minimum edges that must be deleted from a subgraph of order $n$ to render it bipartite.

Contents

• Definitions: bipartiteDistance (the minimum number of edges to delete to reach a bipartite graph) and hG.
• Main open theorem: $h_G(n)/n \to \infty$ as $n \to \infty$.
• Lower and upper bound variants (Erdős-Hajnal-Szemerédi).
• Erdős's conjectured sharper bound.

Assisted by Claude (Anthropic).

[henrykmichalewski]

Closes #341

[Paul-Lez]

Does ∀ C, ∃ n, C * n < hG G n quite capture h_G(n)/n → ∞? It gives unboundedness of the ratio, but not eventual growth along atTop. Could you state this using a filter/Tendsto formulation, or at least as ∀ C, ∀ N, ∃ n ≥ N, C * n < ...?

[Paul-Lez]

Is this lower-bound variant meant to be the same assertion as the main open question? It appears to have essentially the same conclusion as erdos_111 but is marked solved. Could you either weaken it to the known theorem you want to record, or keep it open/omit it if the intended statement is exactly the conjecture?

[henrykmichalewski]

Thanks for the review @PaulLez. Pushed 8b0c922 on add-problem-111: (1) the headline now uses Filter.Tendsto … atTop atTop to faithfully express $h_G(n)/n \to \infty$; (2) the lower_bound variant has been weakened to the actually-known fact $\exists c > 0,, c \cdot n \leq h_G(n)$ eventually, so it is no longer indistinguishable from the open headline.

[mo271]

Nice formalization with well-chosen definitions! A few issues:

1. Erdős conjecture variant uses = ℵ₁ but source says ≥ ℵ₁

The erdos_conjecture variant (line 167) states the upper bound for graphs with chromaticCardinal = ℵ_ 1, but the source explicitly says "for every graph $G$ with chromatic number $\geq \aleph_1$ and every $n$". This matters because a graph with larger chromatic number could potentially have denser subgraphs, so the bound for = ℵ₁ doesn't immediately imply the bound for ≥ ℵ₁. Consider using ℵ_ 1 ≤ G.chromaticCardinal.

2. Misleading docstring for lower_bound

Line 53 says "$h_G(n) \gg n$: this holds (with $h_G(n)/n \to \infty$)". But if $h_G(n)/n \to \infty$ were known, the main problem (which is labeled OPEN) would already be solved. The known result is just the linear lower bound $h_G(n) \geq cn$ for some constant $c > 0$, not super-linear growth. Please fix the parenthetical to avoid confusion.

3. Problem statement repeated

The problem appears in the verbatim quote (line 23) and again in the "Problem statement" section (lines 43–47). It should appear only once.

4. Missing cross-reference to Problem 74

The source page explicitly says "See also [74]", but the file doesn't mention this related

[henrykmichalewski]

Thanks @mo271 for the review. Pushed 24ca0f9 addressing all four points:

1. erdos_conjecture variant uses ≥ ℵ_1. Changed the hypothesis from G.chromaticCardinal = ℵ_ 1 to ℵ_ 1 ≤ G.chromaticCardinal to match the source ("for every graph G with chromatic number ≥ ℵ_1 and every n"). Updated the docstring accordingly to note that ≥ ℵ_1 is the correct quantification (a graph with larger chromatic cardinal is still required to satisfy the bound).

2. Clarified lower_bound docstring. Reworded to state plainly that the linear lower bound h_G(n) ≥ c·n is the known result (no longer claims h_G(n)/n → ∞, which would solve the open problem). Added a sentence clarifying that the open question is precisely whether the linear lower bound can be improved to super-linear.

3. Deduped problem statement. Trimmed the module docstring to the title + *References:* block; removed the ## Problem statement and ## Known results sections (these were verbatim duplicates of content already in the erdos_111 and variant docstrings).

4. Cross-reference to Problem 74. Added "See also Erdős Problem [74]." to the module docstring per the source.

Local lake build FormalConjectures.ErdosProblems.«111» succeeds.