For which graphs $G_{1}, G_{2}$ is it true that for every $n \geq 1$ there is a graph $H$ without a $G_{1}$ but if the edges of $H$ are $n$ -coloured then there is a monochromatic copy of $G_{2}$ , and yet for every graph $H$ without a $G_{1}$ there is an $ℵ_{0}$ -colouring of the edges of $H$ without a monochromatic $G_{2}$ .

Worked, still open.

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

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

Write (H\to (G_2)^E_n) to mean: **every** $n$-edge-colouring of $H$ contains a **monochromatic** copy of (G_2) (as a subgraph). Your two bullets ask for pairs $(G_1,G_2)$ such that

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_596 :
    ∀ {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂),
      IsErdosHajnalExceptional G₁ G₂ ↔
      (answer(sorry) : ∀ {U₁ U₂ : Type}, SimpleGraph U₁ → SimpleGraph U₂ → Prop) G₁ G₂

formal-conjectures/596.lean ↗

status

open

evidence

formal

status

Search Vela