Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×ramsey theory ×Clear all

Problem ledger

9 problemsGraph view
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 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 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 proved (Lean) · formalized · $100erdos:582
True ↔ ∃ V x G, G.CliqueFree 4 ∧ Erdos582.EdgeRamseyTriangle G
graph theoryramsey theoryN/A5 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 proved (Lean) · formalizederdos:966
Let k,r≥2k,r\geq 2. Does there exist a set A⊆NA\subseteq \mathbb{N} that contains no non-trivial arithmetic progression of length k+1k+1, yet in any rr-colouring of AA there must exist a monochromatic non-trivial arithmetic progression of length kk? 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