Vela Mathematics Program: problems

Narrowed toadditive combinatorics ×Clear all

Problem ledger

102 problems · 2/3Number SourcesGraph view

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

Erdős problem 656

number theoryadditive combinatoricsN/A

declared proved (Lean)erdos:658

Erdős problem 658

additive combinatoricspossible4 sources

declared disproved (Lean) · formalized · $1000erdos:707

Erdős conjectured, in over a dozen papers spanning 1976 to 1997 and with a 1000 dollars prize attached, that every finite Sidon set extends to a perfect difference set modulo

p^2+p+1

for some prime

p

. Alexeev and Mixon establish that

\{1,2,4,8\}

is a counterexample - and discovered along the way that Marshall Hall, Jr. had published a different counterexample three decades before Erdős first posed the problem, unnoticed by the community for half a century.

additive combinatoricssidon setsN/A6 sources

declared solvederdos:721

Erdős problem 721

number theoryadditive combinatoricsramsey theoryA171081

declared solved (Lean) · formalizederdos:741

True ↔ ∀ (A : Set ℕ), 0 < (A + A).upperDensity → ∃ A₁ A₂, A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ 0 < (A₁ + A₁).upperDensity ∧ 0 < (A₂ + A₂).upperDensity

additive combinatoricsN/A6 sources

declared open · formalizederdos:749

True ↔ ∀ ε > 0, ∃ A, 1 - ε ≤ (A + A).lowerDensity ∧ (Nat.cast ∘ AdditiveCombinatorics.sumRep A) =O[Filter.atTop] fun n => 1

additive combinatoricsN/A3 sources

declared disprovederdos:763

Erdős problem 763

number theoryadditive combinatoricsN/A

declared disprovederdos:764

Erdős problem 764

number theoryadditive combinatoricsN/A

declared provederdos:772

Erdős problem 772

number theorysidon setsadditive combinatoricspossible

declared disprovederdos:781

Erdős problem 781

additive combinatoricspossible

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

Erdős problem 787

additive combinatoricspossible

declared openerdos:788

Erdős problem 788

additive combinatoricspossible3 sources

declared open · formalizederdos:789

(fun n => ↑(Erdos789.subsetSumThreshold n)) =Θ[Filter.atTop] sorry

additive combinatoricspossible2 sources

declared openerdos:790

Erdős problem 790

additive combinatoricspossible

declared openerdos:791

Erdős problem 791

additive combinatoricsA066063

declared openerdos:792

Erdős problem 792

additive combinatoricspossible2 sources

declared provederdos:806

Erdős problem 806

additive combinatoricspossible

declared disprovederdos:808

Erdős problem 808

additive combinatoricsgraph theoryN/A

declared open · formalizederdos:817

True ↔ (fun n => 3 ^ n) =O[Filter.atTop] fun n => ↑(Erdos817.g 3 n)

additive combinatoricspossible2 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 openerdos:819

Erdős problem 819

additive combinatoricspossible2 sources

declared openerdos:840

Erdős problem 840

additive combinatoricssidon setsN/A

declared disproved · formalizederdos:847

False ↔ ∀ (A : Set ℕ), Infinite ↑A → Erdos847.HasFew3APs A → ∃ n S, (∀ (i : Fin n), ThreeAPFree (S i)) ∧ A = ⋃ i, S i

additive combinatoricsN/A3 sources

declared provederdos:863

Erdős problem 863

number theorysidon setsadditive combinatoricsN/A3 sources

declared openerdos:864

Erdős problem 864

number theorysidon setsadditive combinatoricsA3891822 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 openerdos:866

Estimate the least excess

g_k(N)

forcing

k

integers whose pairwise sums all lie in a dense subset of

\{1, \dots, 2N\}

; in particular, determine the positive variant

h_4(n)

number theoryadditive combinatoricspossible5 sources

declared disproved (Lean) · formalizederdos:867

False ↔ ∃ C, ∀ (N : ℕ), ∀ A ⊆ Finset.Icc 1 N, Erdos867.ConsecutiveSumFree A → ↑A.card ≤ ↑N / 2 + C

additive combinatoricspossible5 sources

declared provederdos:874

Erdős problem 874

number theoryadditive combinatoricspossible

declared openerdos:875

Erdős problem 875

additive combinatoricsN/A2 sources

declared openerdos:876

Erdős problem 876

additive combinatoricsN/A

declared provederdos:877

Erdős problem 877

additive combinatoricsA121269 · possible

declared provederdos:895

Erdős problem 895

additive combinatoricsgraph theoryN/A

declared proved · formalizederdos:899

True ↔ ∀ (A : Set ℕ), A.Infinite → Filter.Tendsto (fun N => ↑(A ∩ Set.Icc 1 N).ncard / ↑N) Filter.atTop (nhds 0) → Filter.limsup (fun N => ↑((A - A) ∩ Set.Icc 1 N).ncard / ↑(A ∩ Set.Icc 1 N).ncard) Filter.atTop = ⊤

additive combinatoricsN/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:984

Erdős problem 984

arithmetic progressionsadditive combinatoricsN/A

declared open · formalizederdos:1097

False ↔ ∃ C > 0, ∀ (A : Finset ℤ), ↑(Erdos1097.CommonDifferencesThreeTermAP A).ncard ≤ C * ↑A.card ^ (3 / 2)

number theoryadditive combinatoricsN/A3 sources

declared open (Lean)erdos:1112

Erdős problem 1112

additive combinatoricsN/A

declared open · formalizederdos:1145

True ↔ Erdos1145.Erdos1145Prop

additive combinatoricsadditive basisN/A2 sources

declared provederdos:1179

Erdős problem 1179

additive combinatoricsprobabilityN/A

declared solvederdos:1185

Erdős problem 1185

additive combinatoricsarithmetic progressionsN/A

declared openerdos:1186

What is the minimum asymptotic density

\delta_k

of monochromatic

k

-term arithmetic progressions in every two-colouring of

\{1, \dots, n\}

? The exact certificate gives

\delta_3 = 117/2192

, matching the known 548-bead colouring.

additive combinatoricsarithmetic progressionspossible2 sources

declared solvederdos:1187

Erdős problem 1187

number theoryprimesadditive combinatoricsN/A3 sources

declared open · $1000erdos:1191

Erdős problem 1191

additive combinatoricssidon setspossible

declared open · formalizederdos:1192

True ↔ ∀ r ≥ 2, ∃ A, (∀ᶠ (n : ℕ) in Filter.atTop, Erdos1192.f_r A r n > 0) ∧ (fun x => ∑ n ∈ Finset.range (x + 1), ↑(Erdos1192.f_r A r n) ^ 2) =O[Filter.atTop] fun x => ↑x

additive combinatoricsadditive basispossible2 sources

declared solved (Lean) · formalizederdos:1193

False ↔ ∀ (A : Set ℕ) (g : ℕ → ℕ), Monotone g → (∀ (n : ℕ), 0 < g n) → {n | AdditiveCombinatorics.sumRep A n = g n}.lowerDensity = 0

additive combinatoricsN/A5 sources

declared openerdos:1194

Erdős problem 1194

additive combinatoricsadditive basissidon setspossible2 sources

declared disprovederdos:1198

Erdős problem 1198

additive combinatoricsramsey theoryN/A

Problems · Vela Mathematics Program

Problem ledger