Vela Mathematics Program: problems

Narrowed toramsey theory ×Clear all

Problem ledger

114 problems · 2/3Number SourcesGraph view

declared openerdos:557

Erdős problem 557

graph theoryramsey theoryN/A

declared openerdos:558

Erdős problem 558

graph theoryramsey theorypossible

declared disprovederdos:559

Erdős problem 559

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

Erdős problem 565

graph theoryramsey theorypossible

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

Erdős problem 570

graph theoryramsey theoryN/A

declared proved (Lean) · formalized · $100erdos:582

True ↔ ∃ V x G, G.CliqueFree 4 ∧ Erdos582.EdgeRamseyTriangle G

graph theoryramsey theoryN/A5 sources

declared proved · formalized · $250erdos:590

OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0) (Ordinal.omega0 ^ Ordinal.omega0) 3

set theoryramsey theoryN/A2 sources

declared proved · formalized · $250erdos:591

True ↔ OrdinalCardinalRamsey (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) (Ordinal.omega0 ^ Ordinal.omega0 ^ 2) 3

set theoryramsey theoryN/A3 sources

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 disproved · formalizederdos:615

False ↔ ∃ c, 0 < c ∧ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (G : SimpleGraph (Fin n)), (1 / 8 - c) * ↑n ^ 2 ≤ ↑G.edgeFinset.card → ¬G.CliqueFree 4 ∨ ↑n / Real.log ↑n ≤ ↑G.indepNum

graph theoryramsey theorypossible2 sources

declared provederdos:636

Erdős problem 636

graph theoryramsey theoryN/A

declared provederdos:637

Erdős problem 637

graph theoryramsey theoryN/A

declared openerdos:638

Erdős problem 638

graph theoryramsey theoryN/A

declared proved (Lean) · formalizederdos:639

True ↔ ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (C : Sym2 (Fin n) → Fin 2), {e | ¬e.IsDiag ∧ ∀ (x y : Fin n), e = s(x, y) → ¬∃ z, z ≠ x ∧ z ≠ y ∧ C s(x, z) = C e ∧ C s(y, z) = C e}.ncard ≤ n ^ 2 / 4

graph theoryramsey theoryN/A5 sources

declared proved (Lean) · formalizederdos:645

∀ (c : ℕ → Bool), ∃ x d, 0 < x ∧ x < d ∧ ∃ C, c x = C ∧ c (x + d) = C ∧ c (x + 2 * d) = C

number theoryadditive combinatoricsramsey theoryN/A5 sources

declared openerdos:667

Erdős problem 667

graph theoryramsey theoryN/A

declared proved · $100erdos:720

Erdős problem 720

graph theoryramsey theorypossible

declared solvederdos:721

Erdős problem 721

number theoryadditive combinatoricsramsey theoryA171081

declared provederdos:800

Erdős problem 800

graph theoryramsey theoryN/A

declared provederdos:801

Erdős problem 801

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

Erdős problem 894

number theoryramsey theoryN/A

declared openerdos:911

Erdős problem 911

graph theoryramsey theoryN/A

declared provederdos:924

Erdős problem 924

graph theoryramsey theoryN/A

declared disprovederdos:925

Erdős problem 925

graph theoryramsey theorypossible

declared solvederdos:948

Erdős problem 948

number theoryramsey theoryN/A3 sources

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

declared disproved · formalizederdos:965

False ↔ ∀ (f : ℝ → Fin 2), ∃ A, ¬A.Countable ∧ ∀ a ∈ A, ∀ b ∈ A, ∀ c ∈ A, ∀ d ∈ A, a ≠ b → c ≠ d → f (a + b) = f (c + d)

ramsey theoryN/A2 sources

declared proved (Lean) · formalizederdos:966

Let

k,r\geq 2

. Does there exist a set

A\subseteq \mathbb{N}

that contains no non-trivial arithmetic progression of length

k+1

, yet in any

r

-colouring of

A

there must exist a monochromatic non-trivial arithmetic progression of length

k

? Answered in the affirmative.

number theoryadditive combinatoricsramsey theoryN/A6 sources

declared provederdos:986

Erdős problem 986

graph theoryramsey theoryA000791 · A0594423 sources

declared solvederdos:1015

Erdős problem 1015

graph theoryramsey theorypossible

declared open · $100erdos:1029

Erdős problem 1029

graph theoryramsey theoryA059442

declared openerdos:1030

Erdős problem 1030

graph theoryramsey theoryA000791 · A059442

declared proved (Lean) · formalizederdos:1090

True ↔ ∀ (k : ℕ), 3 ≤ k → ∃ A, ∀ (C : ↥A → Fin 2), ∃ S, ∃ (hSA : S ⊆ A), Collinear ℝ ↑S ∧ S.card ≥ k ∧ (∀ y ∈ A, y ∈ affineSpan ℝ ↑S → y ∈ S) ∧ ∃ c, ∀ (x : Fin 2 → ℝ) (hx : x ∈ S), C ⟨x, ⋯⟩ = c

geometryramsey theoryN/A5 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science