Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×chromatic number ×Clear all

Problem ledger

22 problemsGraph view
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
Erdos Problem #593 asks which finite triple systems occur in every uncountably chromatic triple system. The answer is exactly the class generated from private-vertex expansions of finite bipartite graphs by finite disjoint unions and one-point amalgamations. Problem #1177 on exact spectra is settled alongside it.
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