erdős #61
For any graph is there some such that every graph on vertices that does not contain as an induced subgraph contains either a complete graph or independent set on vertices?
Worked, still open.
graph theory · open · formalized (Lean) · 0 attempts
machinery: graph-coloring,ramsey-theory,induced-subgraph-free,erdos-hajnal,homogeneous-set-bound,extremal-graph-theory,vertex-substitution-closure
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
unverified AI candidates (2)
gpt-erdos · GPT-5.2 Pro + Deep Research · unverified
What you’re asking is exactly the **Erdős–Hajnal conjecture**.
candidate solution ↗llm-hunter · gpt 5.2, gpt pro 5.2 · unverified
3 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.
candidate solution ↗formal
AMS 5 · open (literature)
theorem erdos_61 :
answer(sorry) ↔ ∀ {α : Type*} [Fintype α] [DecidableEq α] (H : SimpleGraph α),
∃ c > (0 : ℝ), IsErdosHajnalLowerBound H (fun n : ℕ => (n : ℝ) ^ c)formal-conjectures/61.lean ↗links
PhD thesis · paper
#80 in Extremal Graph Theory · link
status
open