Problems · Vela Mathematics Program

declared provederdos:57

Erdős problem 57

declared provederdos:58

Erdős problem 58

declared provederdos:63

Erdős problem 63

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

declared open · formalized · $500erdos:74

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 disprovederdos:110

Erdős problem 110

graph theorychromatic numberset theoryN/A

declared openerdos:111

Erdős problem 111

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 open · $1000erdos:625

Erdős problem 625

declared openerdos:626

Erdős problem 626

graph theorychromatic numbercyclespossible

declared openerdos:627

Erdős problem 627

∀ (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

declared falsifiable · formalizederdos:628

graph theorychromatic numberN/A2 sources

declared openerdos:629

Erdős problem 629

graph theorychromatic numberpossible2 sources

declared provederdos:630

Erdős problem 630

declared provederdos:631

Erdős problem 631

declared disprovederdos:632

Erdős problem 632

declared openerdos:640

Erdős problem 640

graph theorygeometrychromatic numberN/A

declared openerdos:704

Erdős problem 704

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 openerdos:706

Erdős problem 706

declared not provableerdos:736

Erdős problem 736

declared provederdos:737

Erdős problem 737

declared openerdos:738

Erdős problem 738

declared not provableerdos:739

Erdős problem 739

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

declared open · formalizederdos:740

graph theorychromatic numberN/A2 sources

declared disprovederdos:744

Erdős problem 744

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

declared proved (Lean) · formalizederdos:750

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

declared disproved (Lean) · formalizederdos:751

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

declared disproved (Lean) · formalizederdos:753

declared solvederdos:758

Erdős problem 758

declared solvederdos:759

Erdős problem 759

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

declared proved (Lean) · formalizederdos:760

declared openerdos:761

Erdős problem 761

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

declared disproved (Lean) · formalizederdos:762

combinatoricshypergraphschromatic numberN/A

declared provederdos:780

Erdős problem 780

declared provederdos:797

Erdős problem 797

declared provederdos:799

Erdős problem 799

declared disprovederdos:832

Erdős problem 832

graph theoryhypergraphschromatic numberpossible

declared provederdos:833

Erdős problem 833

graph theoryhypergraphschromatic numberpossible

declared openerdos:836

Erdős problem 836

graph theoryhypergraphschromatic numberN/A2 sources

declared provederdos:842

Erdős problem 842

declared openerdos:917

Erdős problem 917

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

declared open · formalizederdos:918

graph theorychromatic numberN/A2 sources

declared openerdos:919

Erdős problem 919

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)

declared solved · formalizederdos:920

graph theorychromatic numberpossible2 sources

declared provederdos:921

Erdős problem 921

graph theorychromatic numbercyclespossible

declared provederdos:922

Erdős problem 922