Is there a graph of chromatic number $ℵ_{1}$ with $ℵ_{1}$ vertices such that for all $ϵ > 0$ if $n$ is sufficiently large and $H$ is a subgraph on $n$ vertices then $H$ contains an independent set of size $> n^{1 - ϵ}$ ? What about an independent set of size $≫ n$ ?

Worked, still open.

graph theory · open · formalized (Lean) · 0 attempts

machinery: graph-coloring,infinite-chromatic-number,set-theory-cardinals,Ramsey-independence-number,extremal-graph-theory

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

A result of Chris Lambie‑Hanson gives much more than what you ask. He proves that for **every** function (f:\mathbb N\to\mathbb N) there is a graph $G$ with [ \chi(G)=\aleph_1 ] (sindeed (|G|=2^{\aleph_1})) such that for every (k\ge 3),

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

2 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 5 · open (literature)

theorem erdos_75 :
    answer(sorry) ↔
    ∃ (V : Type) (G : SimpleGraph V),
      G.chromaticCardinal = ℵ_ 1 ∧
      #V = ℵ_ 1 ∧
      ∀ ε > (0 : ℝ),
        ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : G.Subgraph),
            H.verts.ncard = n →
            ∃ (I : Finset V),
              (I : Set V) ⊆ H.verts ∧
              G.IsIndepSet (I : Set V) ∧
              (I.card : ℝ) > (n : ℝ) ^ (1 - ε)

formal-conjectures/75.lean ↗

status

open

evidence

formal

status

Search Vela