Vela Mathematics Program: problems

Narrowed toformalized ×ramsey theory ×Clear all

Problem ledger

declared proved (Lean) · formalizederdos:45

True ↔ ∀ (k : ℕ), 2 ≤ k → ∃ n, ∀ (colouring : ℕ → Fin k), ∃ colour, ∃ D' ⊆ {d ∈ n.divisors | 1 < d ∧ d < n}, (∀ d ∈ D', colouring d = colour) ∧ D'.reciprocalSum = 1

number theoryunit fractionsramsey theorypossible4 sources

declared proved (Lean) · formalizederdos:46

True ↔ ∀ (𝓒 : ℕ → ℕ), (Set.range 𝓒).Finite → ∃ S, (∀ n ∈ S, 2 ≤ n) ∧ ∑ n ∈ S, 1 / ↑n = 1 ∧ (𝓒 '' ↑S).Subsingleton

number theoryunit fractionsramsey theoryN/A4 sources

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 · 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 open (Lean) · formalized · $250erdos:183

Let

R(3;k)

be the least

n

such that every

k

-colouring of the edges of

K_n

contains a monochromatic triangle. Determine

\lim_{k\to\infty} R(3;k)^{1/k}

(a $250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.

graph theoryramsey theoryA0033233 sources

declared open · formalizederdos:188

IsLeast Erdos188.s sorry

geometryramsey theoryN/A2 sources

declared disproved (Lean) · formalizederdos:189

False ↔ Erdos189.Erdos189For (fun a b c d => (affineSpan ℝ {a, b}).direction ⟂ (affineSpan ℝ {b, c}).direction ∧ (affineSpan ℝ {b, c}).direction ⟂ (affineSpan ℝ {c, d}).direction ∧ (affineSpan ℝ {c, d}).direction ⟂ (affineSpan ℝ {d, a}).direction) fun a b c d => dist a b * dist b c

geometryramsey theoryN/A5 sources

declared proved (Lean) · formalizederdos:484

∃ c, 0 < c ∧ ∀ (k : ℕ), 0 < k → ∃ N₀, ∀ (N : ℕ), N₀ ≤ N → ∀ (f : ℕ → Fin k), c * ↑N ≤ ↑{n ∈ Finset.Icc 1 N | ∃ a ∈ Finset.Icc 1 N, ∃ b ∈ Finset.Icc 1 N, a ≠ b ∧ f a = f b ∧ a + b = n}.card

number theoryadditive combinatoricsramsey theoryN/A5 sources

declared open · formalizederdos:508

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

geometryramsey theoryN/A2 sources

declared proved (Lean) · formalizederdos:532

True ↔ ∀ (c : ℕ → Fin 2), ∃ A, A.Infinite ∧ ∃ color, ∀ (S : Finset ℕ), S.Nonempty → ↑S ⊆ A → c (∑ n ∈ S, n) = color

number theoryramsey theoryN/A4 sources

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

declared proved · formalizederdos:1105

True ↔ ∀ (k : ℕ), 3 ≤ k → (fun n => ↑((SimpleGraph.cycleGraph k).antiRamseyNum n) - ((↑k - 2) / 2 + 1 / (↑k - 1)) * ↑n) =O[Filter.atTop] fun x => 1

graph theoryramsey theorypossible3 sources

declared disproved · formalized · $50erdos:1128

False ↔ ∀ (A B C : Type), Cardinal.mk A = Cardinal.aleph 1 → Cardinal.mk B = Cardinal.aleph 1 → Cardinal.mk C = Cardinal.aleph 1 → ∀ (f : A → B → C → Fin 2), ∃ A₁ B₁ C₁, Cardinal.mk ↑A₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑B₁ = Cardinal.aleph 0 ∧ Cardinal.mk ↑C₁ = Cardinal.aleph 0 ∧ Erdos1128.IsMonochromaticBox f A₁ B₁ C₁

set theoryramsey theoryhypergraphsN/A2 sources

declared open · formalizederdos:1199

True ↔ ∀ (color : ℕ → Fin 2), ∃ A, A.Infinite ∧ ∀ n ∈ A + A, ∀ m ∈ A + A, color n = color m

additive combinatoricsramsey theorypossible2 sources

Problems · Vela Mathematics Program

Problem ledger