Vela Mathematics Program: problems

Narrowed toopen ×ramsey theory ×Clear all

Problem ledger

59 problems · 1/2Number SourcesGraph view

declared open · formalizederdos:70

True ↔ ∀ (β : Ordinal.{0}) (n : ℕ), β.card ≤ Cardinal.aleph0 → 2 ≤ n → Erdos70.OrdinalCardinalRamsey3 Cardinal.continuum.ord β ↑n

graph theoryramsey theoryset theoryN/A2 sources

declared open · $250erdos:77

Erdős problem 77

graph theoryramsey theoryA059442

declared open · $100erdos:78

Erdős problem 78

graph theoryramsey theoryA0594422 sources

declared openerdos:80

Erdős problem 80

graph theoryramsey theoryN/A

declared openerdos:87

Erdős problem 87

graph theoryramsey theoryA059442 · possible

declared openerdos:112

Erdős problem 112

graph theoryramsey theorypossible

declared openerdos:129

Erdős problem 129

graph theoryramsey theorypossible

declared openerdos:159

Erdős problem 159

graph theoryramsey theorypossible

declared open · $500erdos:161

Erdős problem 161

combinatoricsramsey theorydiscrepancyN/A2 sources

declared openerdos:162

Erdős problem 162

combinatoricsramsey theorydiscrepancyN/A

declared open · $250erdos:165

Erdős problem 165

graph theoryramsey theoryA0007912 sources

declared open · formalizederdos:172

True ↔ ∀ (n : ℕ) (color : ℕ → Fin n) (m : ℕ), ∃ A, A.card ≥ m ∧ ∃ c, ∀ (S : Finset ↥A), S.Nonempty → color (∑ x ∈ S, ↑x) = c ∧ color (∏ x ∈ S, ↑x) = c

additive combinatoricsramsey theoryN/A2 sources

declared openerdos:173

Erdős problem 173

geometryramsey theoryN/A

declared openerdos:174

Erdős problem 174

geometryramsey theoryN/A

declared openerdos:181

Erdős problem 181

graph theoryramsey theorypossible

declared openerdos:187

Erdős problem 187

additive combinatoricsramsey theoryN/A

declared open · formalizederdos:188

IsLeast Erdos188.s sorry

geometryramsey theoryN/A2 sources

declared openerdos:483

Erdős problem 483

number theoryadditive combinatoricsramsey theoryA030126

declared open · formalizederdos:508

4 ≤ (SimpleGraph.UnitDistancePlaneGraph Set.univ).chromaticNumber

geometryramsey theoryN/A2 sources

declared openerdos:531

Erdős problem 531

number theoryramsey theorypossible

declared openerdos:544

Erdős problem 544

graph theoryramsey theoryA000791

declared openerdos:545

Erdős problem 545

graph theoryramsey theoryA059442 · possible

declared openerdos:550

Let

m_1\leq\cdots\leq m_k

and

n

be sufficiently large. If

T

is a tree on

n

vertices and

G

is the complete multipartite graph with vertex class sizes

m_1,\ldots,m_k

, prove that

R(T,G)\leq (\chi(G)-1)(R(T,K_{m_1,m_2})-1)+m_1

graph theoryramsey theoryN/A4 sources

declared openerdos:552

Erdős problem 552

graph theoryramsey theoryA006672

declared openerdos:554

Erdős problem 554

graph theoryramsey theorypossible

declared openerdos:555

Erdős problem 555

graph theoryramsey theoryA389313 · possible

declared openerdos:557

Erdős problem 557

graph theoryramsey theoryN/A

declared openerdos:558

Erdős problem 558

graph theoryramsey theorypossible

declared openerdos:560

Erdős problem 560

graph theoryramsey theorypossible

declared openerdos:561

Erdős problem 561

graph theoryramsey theoryN/A

declared open · formalizederdos:562

True ↔ ∀ r ≥ 3, (fun n => Real.log^[r - 1] ↑(Combinatorics.hypergraphRamsey r n)) =Θ[Filter.atTop] fun n => ↑n

graph theoryramsey theoryhypergraphspossible2 sources

declared openerdos:563

Erdős problem 563

graph theoryramsey theoryhypergraphsN/A

declared open · formalized · $500erdos:564

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ 2 ^ (c * n) ≤ ↑(Combinatorics.hypergraphRamsey 3 n)

graph theoryramsey theoryhypergraphspossible2 sources

declared open · formalizederdos:566

True ↔ ∀ (p : ℕ) (G : SimpleGraph (Fin p)), (∀ (S : Finset (Fin p)), 2 ≤ S.card → (SimpleGraph.induce (↑S) G).edgeSet.ncard ≤ 2 * S.card - 3) → ∃ c > 0, ∀ (n : ℕ) (H : SimpleGraph (Fin n)) [inst : DecidableRel H.Adj], (∀ (v : Fin n), 0 < H.degree v) → ↑(G.sizeRamsey H) ≤ c * ↑H.edgeSet.ncard

graph theoryramsey theoryN/A2 sources

declared open · formalizederdos:567

True ↔ Erdos567.Q3.IsRamseySizeLinear

graph theoryramsey theoryN/A2 sources

declared openerdos:568

Erdős problem 568

graph theoryramsey theoryN/A

declared openerdos:569

Erdős problem 569

graph theoryramsey theoryN/A

declared open · formalized · $1000erdos:592

∀ (β : Ordinal.{u}), β.card ≤ Cardinal.aleph0 → OrdinalCardinalRamsey (Ordinal.omega0 ^ β) (Ordinal.omega0 ^ β) 3 ↔ sorry β

set theoryramsey theoryN/A2 sources

declared open · formalizederdos:596

∀ {U₁ U₂ : Type} (G₁ : SimpleGraph U₁) (G₂ : SimpleGraph U₂), G₁.IsErdosHajnalExceptional G₂ ↔ (fun {U₁ U₂} => sorry) G₁ G₂

graph theoryramsey theoryset theoryN/A2 sources

declared openerdos:597

Erdős problem 597

graph theoryramsey theoryset theoryN/A

declared open · formalizederdos:598

∀ (m : Type u_1) [Infinite m], True ↔ ∃ c, ∀ (X : Set m), Cardinal.mk ↑X = Erdos598.κ → c '' {s | ↑s ⊆ X} = Set.univ

set theoryramsey theoryN/A3 sources

declared openerdos:609

Erdős problem 609

graph theoryramsey theorypossible

declared openerdos:638

Erdős problem 638

graph theoryramsey theoryN/A

declared openerdos:667

Erdős problem 667

graph theoryramsey theoryN/A

declared openerdos:809

Erdős problem 809

graph theoryramsey theorypossible

declared openerdos:810

Erdős problem 810

graph theoryramsey theorypossible

declared openerdos:811

Erdős problem 811

graph theoryramsey theorypossible

declared open · formalizederdos:812

True ↔ ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ↑(Combinatorics.hypergraphRamsey 2 (n + 1)) / ↑(Combinatorics.hypergraphRamsey 2 n) ≥ 1 + c

graph theoryramsey theoryA0594422 sources

declared openerdos:911

Erdős problem 911

graph theoryramsey theoryN/A

declared open · formalizederdos:949

True ↔ ∀ (S : Set ℝ), (∀ a ∈ S, ∀ b ∈ S, a + b ∉ S) → ∃ A ⊆ Sᶜ, Cardinal.mk ↑A = Cardinal.continuum ∧ A + A ⊆ Sᶜ

ramsey theoryN/A3 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science