Vela Mathematics Program: problems

Narrowed tograph theory ×Clear all

Problem ledger

275 problems · 5/6Number SourcesGraph view

declared provederdos:816

Erdős problem 816

graph theoryN/A

declared disprovederdos:832

Erdős problem 832

graph theoryhypergraphschromatic numberpossible

declared provederdos:833

Erdős problem 833

graph theoryhypergraphschromatic numberpossible

declared solvederdos:834

Erdős problem 834

graph theoryhypergraphsN/A

declared verifiable · formalizederdos:835

∀ {k : ℕ}, 3 ≤ k → k ≤ 8 → ↑k + 1 < (SimpleGraph.johnson (2 * k) k).chromaticNumber

graph theoryhypergraphsN/A3 sources

declared openerdos:836

Erdős problem 836

graph theoryhypergraphschromatic numberN/A2 sources

declared openerdos:837

Erdős problem 837

graph theoryhypergraphsN/A

declared provederdos:842

Erdős problem 842

graph theorychromatic numberN/A

declared openerdos:883

Erdős problem 883

number theorygraph theoryN/A

declared provederdos:895

Erdős problem 895

additive combinatoricsgraph theoryN/A

declared provederdos:900

Erdős problem 900

graph theoryN/A

declared openerdos:902

Erdős problem 902

graph theoryA362137

declared proved (Lean) · formalizederdos:904

True ↔ ∀ (V : Type u_1) [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], ∀ r ∈ Set.Icc 1 (Erdos904.n V), Erdos904.turanNumber (Erdos904.n V) r ≤ G.edgeFinset.card → ∃ s, G.IsNClique r s ∧ 2 * r * G.edgeFinset.card ≤ Erdos904.n V * ∑ v ∈ s, G.degree v

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:905

∀ (n : ℕ) (G : SimpleGraph (Fin n)) [inst : DecidableRel G.Adj], ↑n ^ 2 / 4 < ↑G.edgeFinset.card → ∃ e ∈ G.edgeFinset, ↑n / 6 ≤ ↑(G.trianglesContaining e).card

graph theoryN/A5 sources

declared openerdos:911

Erdős problem 911

graph theoryramsey theoryN/A

declared proved (Lean) · formalizederdos:914

∀ {r m : ℕ}, 2 ≤ r → 1 ≤ m → ∀ {V : Type u_1} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj], Fintype.card V = r * m → m * (r - 1) ≤ G.minDegree → ∃ K, (∀ (i : Fin m), G.IsNClique r (K i)) ∧ Pairwise fun i j => Disjoint (K i) (K j)

graph theoryN/A5 sources

declared solvederdos:915

Erdős problem 915

graph theoryN/A

declared provederdos:916

Erdős problem 916

graph theorycyclesN/A

declared openerdos:917

Erdős problem 917

graph theorychromatic numberN/A

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

Erdős problem 919

graph theorychromatic numberN/A

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 provederdos:921

Erdős problem 921

graph theorychromatic numbercyclespossible

declared provederdos:922

Erdős problem 922

graph theorychromatic numberN/A

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 provederdos:924

Erdős problem 924

graph theoryramsey theoryN/A

declared disprovederdos:925

Erdős problem 925

graph theoryramsey theorypossible

declared provederdos:926

Erdős problem 926

graph theorypossible

declared disproved (Lean)erdos:927

Erdős problem 927

graph theorypossible3 sources

declared openerdos:934

Erdős problem 934

graph theorypossible

declared open · formalizederdos:944

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

graph theorychromatic numberN/A2 sources

declared provederdos:986

Erdős problem 986

graph theoryramsey theoryA000791 · A0594423 sources

declared falsifiableerdos:993

Erdős problem 993

graph theoryA000055 · possible

declared disprovederdos:1006

Erdős problem 1006

graph theorycyclesN/A

declared solved (Lean) · formalizederdos:1007

IsLeast {m | ∃ n G, G.HasDimension 4 ∧ G.edgeSet.ncard = m} sorry

graph theoryN/A5 sources

declared proved (Lean) · formalizederdos:1008

True ↔ ∃ c > 0, ∀ (V : Type) [Fintype V] (G : SimpleGraph V), ∃ H ≤ G, (SimpleGraph.cycleGraph 4).Free H ∧ c * ↑G.edgeSet.ncard ^ (2 / 3) ≤ ↑H.edgeSet.ncard

graph theoryN/A5 sources

declared provederdos:1009

Erdős problem 1009

graph theoryN/A

declared provederdos:1010

Erdős problem 1010

graph theoryN/A

declared openerdos:1011

Erdős problem 1011

graph theorypossible

declared solvederdos:1012

Erdős problem 1012

graph theory

declared openerdos:1013

Erdős problem 1013

graph theoryA292528

declared proved (Lean) · formalizederdos:1014

∀ (k : ℕ), 3 ≤ k → Filter.Tendsto (fun l => ↑R(k, l + 1) / ↑R(k, l)) Filter.atTop (nhds 1)

graph theorypossible7 sources

declared solvederdos:1015

Erdős problem 1015

graph theoryramsey theorypossible

declared openerdos:1016

Erdős problem 1016

graph theorycyclesA105206

declared openerdos:1017

Erdős problem 1017

graph theorypossible

declared solvederdos:1018

Erdős problem 1018

graph theoryplanar graphsN/A

declared provederdos:1019

Erdős problem 1019

graph theoryplanar graphsN/A

declared falsifiableerdos:1020

Erdős problem 1020

graph theoryhypergraphsN/A

declared provederdos:1021

Erdős problem 1021

graph theoryN/A2 sources

declared solvederdos:1024

Erdős problem 1024

graph theoryhypergraphspossible

Problems · Vela Mathematics Program

Problem ledger

Search problems.science