erdős #740
Let be an infinite cardinal and be a graph with chromatic number . Let . Must contain a subgraph of chromatic number which does not contain any odd cycle of length ?
Open — best to date is a honest null, not yet sealed.
graph theory · open · formalized (Lean) · 1 attempt
use this record
vela registry pull vfr_37aec80d874a0239vela reproduce examples/erdos-problemsevidence
honest null
needs verification
attempted via frontier '?' (transfer_strength=n/a) -> no_progress
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
For (r\le 2) the condition is vacuous [[nomath]](simple graphs have no odd cycles of length $1$ or $2$)[[/nomath]], so you can just take $G$ itself.
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_740 :
answer(sorry) ↔
∀ (V : Type*) (G : SimpleGraph V),
ℵ₀ ≤ G.chromaticCardinal →
∀ (r : ℕ),
∃ (H : G.Subgraph), H.coe.chromaticCardinal = G.chromaticCardinal ∧
NoShortOddCycle H.coe rformal-conjectures/740.lean ↗status
open