Vela Mathematics Program: problems

Narrowed toformalized ×sidon sets ×Clear all

Problem ledger

19 problemsGraph view

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 · 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 proved · formalizederdos:152

True ↔ Filter.Tendsto Erdos152.f Filter.atTop Filter.atTop

sidon setsN/A4 sources

declared open · formalizederdos:153

True ↔ Filter.Tendsto Erdos153.f Filter.atTop Filter.atTop

sidon setsN/A2 sources

declared proved (Lean) · formalizederdos:154

True ↔ ∀ (m : ℕ), 2 ≤ m → ∀ (N : ℕ → ℕ) (A : ℕ → Finset ℕ), Filter.Tendsto (fun k => ↑(N k)) Filter.atTop Filter.atTop → (∀ (k x : ℕ), x ∈ A k → x ≤ N k) → (∀ (k : ℕ), IsSidon ↑(A k)) → Filter.Tendsto (fun k => ↑(A k).card / √↑(N k)) Filter.atTop (nhds 1) → ∀ i < m, Filter.Tendsto (fun k => ↑{s ∈ A k + A k | s % m = i}.card / ↑(A k + A k).card) Filter.atTop (nhds (1 / ↑m))

sidon setsN/A6 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:156

True ↔ (fun N => ↑(Erdos156.minMaximalSidonSet N)) =O[Filter.atTop] fun N => ↑N ^ (1 / 3)

sidon setsA3823972 sources

declared open · formalizederdos:158

∀ {A : Set ℕ}, Erdos158.B2 1 A ↔ IsSidon A

sidon setsN/A2 sources

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 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 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 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 open · formalizederdos:757

∀ {A : Set ℝ}, sorry = sSup {c | Erdos757.IsAdmissible c}

geometrydistancessidon setspossible2 sources

declared solved (Lean) · formalizederdos:862

False ↔ (fun N => Real.logb 2 ↑(Erdos862.numMaximalSidonSets N)) =o[Filter.atTop] fun N => ↑N ^ (1 / 2)

number theorysidon setsA3823955 sources

Problems · Vela Mathematics Program

Problem ledger

Search problems.science