Vela Mathematics Program: problems

Narrowed toadditive combinatorics ×Clear all

Problem ledger

102 problems · 1/3Number SourcesGraph view

declared open · formalized · $500erdos:1

∃ C > 0, ∀ (N : ℕ) (A : Finset ℕ), Erdos1.IsSumDistinctSet A N → N ≠ 0 → C * 2 ^ A.card < ↑N

number theoryadditive combinatoricsA2766612 sources

declared open · formalized · $5000erdos:3

True ↔ ∀ (A : Set ℕ), (¬Summable fun a => 1 / ↑↑a) → ∃ᶠ (k : ℕ) in Filter.atTop, ∃ S ⊆ A, S.IsAPOfLength ↑k

number theoryadditive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources

declared open · formalizederdos:14

True ↔ ∀ (A : Set ℕ), ∀ ε > 0, Erdos14.almostSquareRoot ε =O[Filter.atTop] Erdos14.nonUniqueSumCount A

number theorysidon setsadditive combinatoricsA143824 · possible2 sources

declared open · formalized · $1000erdos:30

True ↔ ∀ ε > 0, (fun N => ↑(Erdos30.h N) - √↑N) =O[Filter.atTop] fun N => ↑N ^ ε

number theorysidon setsadditive combinatoricsA143824 · A227590 · A0030222 sources

declared open · formalizederdos:36

Erdos36.M 5 = 3

number theoryadditive combinatoricsA393584 · possible3 sources

declared disprovederdos:37

Erdős problem 37

number theoryadditive combinatoricsN/A

declared open · formalized · $500erdos:39

True ↔ ∃ A, A.Infinite ∧ IsSidon A ∧ ∀ ε > 0, (fun x => ↑x ^ (1 / 2 - ε)) =O[Filter.atTop] fun N => ↑(Set.Icc 1 N ∩ A).ncard

number theorysidon setsadditive combinatoricsN/A2 sources

declared open · formalized · $500erdos:41

∀ (A : Set ℕ), Erdos41.NtupleCondition A 3 → A.Infinite → Filter.liminf (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N ^ (1 / 3)) Filter.atTop = 0

number theorysidon setsadditive combinatoricsN/A2 sources

declared solved (Lean) · formalizederdos:42

True ↔ ∀ M ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, ∀ (A : Set ℕ), A.IsMaximalSidonSetIn N → ∃ B ⊆ Set.Icc 1 N, IsSidon B ∧ B.ncard = M ∧ (A - A) ∩ (B - B) = {0}

number theorysidon setsadditive combinatoricsN/A6 sources

declared disproved · formalized · $100erdos:43

If Sidon sets

A, B \subseteq \{1, \dots, N\}

satisfy

(A-A) \cap (B-B) = \{0\}

, must

\binom{|A|}{2} + \binom{|B|}{2} \le \binom{f(N)}{2} + O(1)

, where

f(N)

is the largest Sidon-set size in

[N]

- and can the bound be improved by a fixed proportion when

|A| = |B|

number theorysidon setsadditive combinatoricsA143824 · A227590 · A003022 · possible4 sources

declared open · formalizederdos:44

True ↔ ∀ N ≥ 1, ∀ A ⊆ Finset.Icc 1 N, IsSidon ↑A → ∀ ε > 0, ∃ M > N, ∃ B ⊆ Finset.Icc (N + 1) M, IsSidon (↑A ∪ ↑B) ∧ (1 - ε) * √↑M ≤ ↑(A ∪ B).card

number theorysidon setsadditive combinatoricsN/A2 sources

declared open · formalized · $250erdos:52

True ↔ ∀ (ε : ℝ), 0 < ε → ε < 1 → ∃ C, 0 < C ∧ ∀ (A : Finset ℤ), max ↑(A + A).card ↑(A * A).card ≥ C * ↑A.card ^ (2 - ε)

number theoryadditive combinatoricsA2639963 sources

declared provederdos:53

Erdős problem 53

number theoryadditive combinatoricspossible

declared proved · formalizederdos:109

∀ (A : Set ℕ), A.upperDensity > 0 → ∃ B C, B.Infinite ∧ C.Infinite ∧ B + C ⊆ A

additive combinatoricsN/A2 sources

declared open · formalized · $500erdos:138

W(k)

is the least

N

such that every two-colouring of

\{1, \dots, N\}

contains a monochromatic

k

-term arithmetic progression, must

W(k+1) - W(k) \to \infty

additive combinatoricsA0053464 sources

declared proved · formalized · $1000erdos:139

∀ (k : ℕ), 1 < k → Filter.Tendsto (fun N => ↑(Erdos139.r k N) / ↑N) Filter.atTop (nhds 0)

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030052 sources

declared proved · $500erdos:140

Erdős problem 140

additive combinatoricsarithmetic progressionsA003002

declared open · formalizederdos:141

sorry ↔ ∀ k ≥ 3, ∃ s, Erdos141.Set.IsAPAndPrimeProgressionOfLength s k

additive combinatoricsprimesarithmetic progressionsA0065602 sources

declared open · formalized · $10000erdos:142

∀ (k : ℕ), (fun N => ↑(Erdos142.r k N)) =Θ[Filter.atTop] sorry

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A0030053 sources

declared open · formalizederdos:155

True ↔ ∀ k ≥ 1, ∀ᶠ (N : ℕ) in Filter.atTop, Erdos155.F (N + k) ≤ Erdos155.F N + 1

additive combinatoricssidon setsA143824 · A227590 · A0030222 sources

declared open · formalizederdos:160

have lower_bound := sorry; (lower_bound =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) ∧ ∀ c > 0, ((fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =O[Filter.atTop] fun n => ↑(Erdos160.erdos_160.h n)) → ∀ c > 0, (fun n => Real.exp (c * Real.log ↑n ^ (1 / 12))) =o[Filter.atTop] lower_bound

additive combinatoricsarithmetic progressionspossible2 sources

declared open · formalizederdos:168

Erdos168.F 0 = 0

additive combinatoricsA004059 · A057561 · A094708 · A3864392 sources

declared openerdos:169

Erdős problem 169

additive combinatoricsarithmetic progressionsA005346

declared open · formalizederdos:170

Filter.Tendsto (fun N => ↑(Erdos170.F N) / √↑N) Filter.atTop (nhds sorry)

additive combinatoricsA0466932 sources

declared provederdos:171

Erdős problem 171

additive combinatoricscombinatoricsA156989

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

Let

N(k, \ell)

be the least

N

such that every

f : [N] \to \{-1, 1\}

has a

k

-term arithmetic progression

P

with

|\sum_{n \in P} f(n)| \ge \ell

. In particular, is

N(k, 2) \le C^k

additive combinatoricsarithmetic progressionsdiscrepancypossible3 sources

declared provederdos:179

Erdős problem 179

additive combinatoricsarithmetic progressionspossible

declared provederdos:185

Erdős problem 185

additive combinatoricsA003142

declared solvederdos:186

Erdős problem 186

additive combinatoricsA389784

declared openerdos:187

Erdős problem 187

additive combinatoricsramsey theoryN/A

declared solvederdos:190

Erdős problem 190

additive combinatoricsarithmetic progressionspossible

declared disproved (Lean) · formalizederdos:198

∀ (V : Type u_1) [inst : AddCommGroup V] [Module ℚ V], ∃ X, (∀ (Y : Set V), Y.IsAPOfLength ⊤ → (X ∩ Y).Nonempty) ∧ ∀ (Y : Set V), Y.IsAPOfLength 3 → (X ∩ Y).ncard ≤ 2

additive combinatoricssidon setsarithmetic progressionsN/A5 sources

declared openerdos:201

Erdős problem 201

additive combinatoricsarithmetic progressionsA003002 · A003003 · A003004 · A003005 · possible

declared proved · formalizederdos:219

∅ ∉ Erdos219.primeArithmeticProgressions

number theoryadditive combinatoricsprimesA005115 · A113827 · A1235562 sources

declared open · formalized · $100erdos:241

True ↔ Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos241.f N 3)) fun N => ↑N ^ (1 / 3)

additive combinatoricssidon setsA3877042 sources

declared proved · formalizederdos:245

True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard / N) Filter.atTop (nhds 0) → 3 ≤ Filter.limsup (fun N => ↑((A + A) ∩ Set.Icc 1 ⌊N⌋₊).ncard / ↑(A ∩ Set.Icc 1 ⌊N⌋₊).ncard) Filter.atTop

additive combinatoricsN/A2 sources

declared openerdos:271

Erdős problem 271

additive combinatoricsarithmetic progressionsA005487

declared open · formalizederdos:272

Asymptotics.IsEquivalent Filter.atTop (fun N => ↑(Erdos272.maxArithInterCard N)) sorry

additive combinatoricsarithmetic progressionspossible2 sources

declared disproved (Lean) · formalizederdos:328

False ↔ ∀ (C : ℕ), 0 < C → ∃ t, ∀ (A : Set ℕ), (∀ (n : ℕ), AdditiveCombinatorics.sumRep A n ≤ C) → ∃ P, ⋃ i, P i = A ∧ Set.univ.PairwiseDisjoint P ∧ ∀ (i : Fin t) (n : ℕ), AdditiveCombinatorics.sumRep (P i) n < C

number theoryadditive combinatoricsN/A4 sources

declared disproved (Lean) · formalizederdos:331

False ↔ ∀ (A B : Set ℕ), ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count A n)) → ((fun n => ↑n ^ (1 / 2)) =O[Filter.atTop] fun n => ↑(Nat.count B n)) → {(a₁, a₂, b₁, b₂) | a₁ ∈ A ∧ a₂ ∈ A ∧ b₁ ∈ B ∧ b₂ ∈ B ∧ a₁ ≠ a₂ ∧ a₁ + b₂ = a₂ + b₁}.Infinite

number theoryadditive combinatoricsN/A5 sources

declared openerdos:335

Erdős problem 335

number theoryadditive combinatoricsN/A2 sources

declared disproved (Lean) · formalizederdos:337

False ↔ ∀ (A : Set ℕ), A.IsAsymptoticAddBasis → ((fun N => ↑(A ∩ Set.Icc 1 N).ncard) =o[Filter.atTop] fun N => ↑N) → Filter.Tendsto (fun N => ↑((A + A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop Filter.atTop

number theoryadditive combinatoricsadditive basisN/A5 sources

declared open · formalizederdos:340

∀ ε > 0, (fun n => √↑n / ↑n ^ ε) =O[Filter.atTop] fun n => ↑(Set.range Finset.greedySidon ∩ Set.Icc 1 n).ncard

number theoryadditive combinatoricssidon setsA080200 · A0052822 sources

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 decidableerdos:475

Erdős problem 475

number theoryadditive combinatoricsN/A

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 openerdos:483

Erdős problem 483

number theoryadditive combinatoricsramsey theoryA030126

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 · formalizederdos:494

∀ (k card p : ℕ), Nat.Prime p → k ∈ Set.Ioo 0 p → p ∣ card → Erdos494.Erdos494Unique k card

analysisadditive combinatoricsN/A2 sources

Problems · Vela Mathematics Program

Problem ledger