erdős #108
For every and is there some finite such that every graph of chromatic number contains a subgraph of girth and chromatic number ?
Open — best to date is a honest null, not yet sealed.
graph theory · open · possible · formalized (Lean) · 1 attempt
machinery: graph-coloring,chromatic-number,girth,Erdos-Hajnal,high-girth-subgraph-extraction,extremal-graph-theory
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
honest null
needs verification
attempted via frontier '?' (transfer_strength=n/a) -> already_known
No solve/partial on this pass. Transfer into the owned frontier was 'n/a'. Do not re-attack cold; needs a new idea or richer accumulated context.
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
This is **open in general**. It is a well‑known conjecture of **Erdős and Hajnal** (sometimes called the Erdős–Hajnal conjecture on large‑girth, large‑chromatic subgraphs) that such a function $f(k,r)$ should exist for **all** (k,r), but it is only proved in a few cases. ([Erdős Problems][1])
candidate solution ↗llm-hunter · gpt pro 5.2 · unverified
1 LLM attack(s) recorded (gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 · open (literature)
theorem erdos_108 :
answer(sorry) ↔ ∀ r ≥ 4, ∀ k ≥ (2 : ℕ), ∃ (f : ℕ),
∀ (V : Type u) (G : SimpleGraph V) (_ : Nonempty V)
(hchro : f ≤ SimpleGraph.chromaticNumber G),
∃ (H : G.Subgraph), (SimpleGraph.girth H.coe ≥ r) ∧
(SimpleGraph.chromaticNumber H.coe ≥ k)formal-conjectures/108.lean ↗links
status
open