Vela Mathematics Program: problems

Narrowed toformalized ×chromatic number ×Clear all

Problem ledger

declared open · formalized · $500erdos:74

∀ {V : Type u} {G : SimpleGraph V} (A : G.Subgraph), (Erdos74.SimpleGraph.edgeDistancesToBipartite A).Nonempty

graph theorychromatic numbercyclesN/A2 sources

declared open · formalizederdos:75

True ↔ ∃ V G, G.chromaticCardinal = Cardinal.aleph 1 ∧ Cardinal.mk V = Cardinal.aleph 1 ∧ ∀ ε > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (H : G.Subgraph), H.verts.ncard = n → ∃ I, ↑I ⊆ H.verts ∧ G.IsIndepSet ↑I ∧ ↑I.card > ↑n ^ (1 - ε)

graph theorychromatic numberN/A3 sources

declared open · formalizederdos:108

True ↔ ∀ r ≥ 4, ∀ k ≥ 2, ∃ f, ∀ (V : Type u) (G : SimpleGraph V), Nonempty V → ↑f ≤ G.chromaticNumber → ∃ H, H.coe.girth ≥ r ∧ H.coe.chromaticNumber ≥ ↑k

graph theorychromatic numbercyclespossible2 sources

declared open · formalizederdos:130

For an infinite planar set in strong general position, how large can the chromatic and clique numbers of its positive-integer-distance graph be - in particular, can the chromatic number be infinite? Yes: there is such a set, no three collinear and no four concyclic, with infinite chromatic number.

graph theorychromatic numberN/A4 sources

declared open · formalized · $500erdos:593

Which finite triple systems occur in every triple system of uncountable chromatic number? The claimed characterization: exactly those that, after removing isolated vertices, are linear, have every hyperedge-node of their Levi graph meeting a bridge, and have every Berge cycle even.

set theorygraph theoryhypergraphsN/A4 sources

declared falsifiable · formalizederdos:628

∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V) (k : ℕ), G.chromaticNumber = ↑k → G.CliqueFree k → ∀ (a b : ℕ), a ≥ 2 → b ≥ 2 → a + b = k + 1 → ∃ s, (SimpleGraph.induce s G).chromaticNumber ≥ ↑a ∧ (SimpleGraph.induce sᶜ G).chromaticNumber ≥ ↑b

graph theorychromatic numberN/A2 sources

declared disproved · formalizederdos:705

False ↔ ∃ k, ∀ (V : Set (EuclideanSpace ℝ (Fin 2))), V.Finite → (SimpleGraph.UnitDistancePlaneGraph V).girth ≥ k → (SimpleGraph.UnitDistancePlaneGraph V).chromaticNumber ≤ 3

graph theorychromatic numberN/A3 sources

declared open · formalizederdos:740

True ↔ ∀ (V : Type u_1) (G : SimpleGraph V), Cardinal.aleph0 ≤ G.chromaticCardinal → ∀ (r : ℕ), ∃ H, H.coe.chromaticCardinal = G.chromaticCardinal ∧ Erdos740.NoShortOddCycle H.coe r

graph theorychromatic numberN/A2 sources

declared proved (Lean) · formalizederdos:750

True ↔ ∀ (f : ℕ → NNReal), Filter.Tendsto f Filter.atTop Filter.atTop → ∃ V G, G.chromaticNumber = ⊤ ∧ ∀ (m : ℕ) (S : Set V), 0 < m → S.ncard = m → ∃ I ⊆ S, G.IsIndepSet I ∧ ↑m / 2 - f m ≤ ↑I.ncard

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:751

False ↔ ∀ (k : ℕ), ∃ V G, G.chromaticNumber = 4 ∧ ∀ m ∈ G.cycleLengths, ∀ m' ∈ G.cycleLengths, m < m' → m + k ≤ m'

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:753

False ↔ ∃ c, 0 < c ∧ ∀ (n : ℕ), 0 < n → ∀ (G : SimpleGraph (Fin n)), ↑n ^ (1 / 2 + c) < ↑(Erdos753.listChromaticNumber G) + ↑(Erdos753.listChromaticNumber Gᶜ)

graph theorychromatic numberN/A5 sources

declared proved (Lean) · formalizederdos:760

True ↔ ∃ c > 0, ∀ (V : Type u_1) [Finite V] (G : SimpleGraph V) (m : ℕ), G.chromaticNumber = ↑m → ∃ H k, ↑k ≤ H.coe.cochromaticNumber ∧ c * ↑m / Real.log ↑m ≤ ↑k

graph theorychromatic numberN/A5 sources

declared disproved (Lean) · formalizederdos:762

False ↔ ∀ (V : Type u_1) [Fintype V] (G : SimpleGraph V), G.CliqueFree 5 → 4 ≤ G.cochromaticNumber → G.chromaticNumber ≤ G.cochromaticNumber + 2

graph theorychromatic numberN/A5 sources

declared open · formalizederdos:918

True ↔ ∃ V G, Cardinal.mk V = Cardinal.aleph 2 ∧ G.chromaticCardinal = Cardinal.aleph 2 ∧ ∀ (W : Set V), Cardinal.mk ↑W = Cardinal.aleph 1 → (SimpleGraph.induce W G).chromaticCardinal ≤ Cardinal.aleph0

graph theorychromatic numberN/A2 sources

declared solved · formalizederdos:920

True ↔ ∀ k ≥ 4, ∃ c > 0, (fun n => ↑n ^ (1 - 1 / (↑k - 1)) / Real.log ↑n ^ c) =O[Filter.atTop] fun n => ↑(Erdos920.f k n)

graph theorychromatic numberpossible2 sources

declared proved (Lean) · formalizederdos:923

True ↔ ∀ (V : Type u_1) (n : ℕ), ∃ k, ∀ (G : SimpleGraph V), ↑k ≤ G.chromaticNumber → ∃ H ≤ G, ↑n ≤ H.chromaticNumber ∧ H.CliqueFree 3

graph theorychromatic numberN/A5 sources

declared open · formalizederdos:944

True ↔ ∀ k ≥ 4, ∀ r ≥ 1, ∃ V G, Erdos944.SimpleGraph.IsErdos944 G k r

graph theorychromatic numberN/A2 sources

declared open · formalizederdos:1068

True ↔ ∀ (V : Type) (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ s, s.Countable ∧ (SimpleGraph.induce s G).InfinitelyConnected

graph theoryset theorychromatic numberN/A2 sources

declared disproved · formalizederdos:1092

False ↔ (fun n => ↑n) =o[Filter.atTop] fun n => ↑(Erdos1092.f 2 n)

geometrychromatic numberN/A5 sources

declared open · formalizederdos:1104

∃ c₁, 0 < c₁ ∧ c₁ ≤ 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, c₁ * √↑n / √(Real.log ↑n) ≤ ↑(Erdos1104.triangleFreeMaxChromatic n)

graph theorychromatic numberA2925282 sources

declared open · formalizederdos:1175

True ↔ ∀ (κ : Cardinal.{u_1}), Cardinal.aleph0 < κ → ∃ μ, ∀ (V : Type u_1) (G : SimpleGraph V), G.chromaticCardinal = μ → ∃ H, H.coe.CliqueFree 3 ∧ H.coe.chromaticCardinal = κ

set theorychromatic numberN/A2 sources

declared not disprovable · formalizederdos:1176

True ↔ ∀ {V : Type u_1} (G : SimpleGraph V), G.chromaticCardinal = Cardinal.aleph 1 → ∃ EColor, ∃ (_ : Cardinal.mk EColor = Cardinal.aleph 1), ∃ c_edge, ∀ (VColor : Type), Cardinal.mk VColor ≤ Cardinal.aleph 0 → ∀ (c_vert : V → VColor), ∃ vc, ∀ (ec : EColor), ∃ u v, ∃ (h : G.Adj u v), c_vert u = vc ∧ c_vert v = vc ∧ c_edge ⟨s(u, v), h⟩ = ec

set theorychromatic numberN/A2 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science