Skip to content

Problems · Vela Mathematics Program

Narrowed toproved (Lean) ×additive combinatorics ×Clear all

Problem ledger

9 problemsGraph view
declared proved (Lean) · formalizederdos:350
∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : DecidableEq M] (A : Finset M), Erdos350.DistinctSubsetSums ↑A ↔ Erdos350.DecidableDistinctSubsetSums A
number theoryadditive combinatoricsN/A5 sources
declared proved (Lean) · formalizederdos:476
True ↔ ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (A : Finset (ZMod p)), A.restrictedSumset.card ≥ min (2 * A.card - 3) p
number theoryadditive combinatoricsN/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 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)erdos:658
Erdős problem 658
additive combinatoricspossible4 sources
declared proved (Lean) · formalizederdos:785
True ↔ ∀ (A B : Set ℕ), A.Infinite → B.Infinite → Erdos785.IsExactAdditiveComplement A B → Filter.Tendsto (fun x => ↑(Erdos785.counting A x) * ↑(Erdos785.counting B x) - ↑x) Filter.atTop Filter.atTop
additive combinatoricsN/A5 sources
declared proved (Lean) · formalizederdos:818
True ↔ ∀ (K : ℝ), 0 < K → ∃ C, 0 < C ∧ ∃ c, 0 < c ∧ ∀ (A : Finset ℤ), 2 ≤ A.card → ↑(A + A).card ≤ K * ↑A.card → c * ↑A.card ^ 2 / Real.log ↑A.card ^ C ≤ ↑(A * A).card
additive combinatoricsN/A5 sources
declared proved (Lean) · formalizederdos:865
∃ C > 0, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ A ⊆ Finset.Icc 1 N, ↑A.card ≥ 5 / 8 * ↑N + C → ∃ a ∈ A, ∃ b ∈ A, ∃ c ∈ A, a ≠ b ∧ a ≠ c ∧ b ≠ c ∧ a + b ∈ A ∧ a + c ∈ A ∧ b + c ∈ A
number theoryadditive combinatoricspossible5 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