Skip to content

Erdős problem 42

Start work

Erdős Problem 42: Let M ≥ 1 and N be sufficiently large in terms of M. Is it true that for every maximal Sidon set A ⊆ {1,…,N} there is another Sidon set B ⊆ {1,…,N} of size M such that (A - A) ∩ (B - B) = {0}?

Sources

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

42.lean

Retained formal statement2 of 5

A variant asking for explicit bounds on how large N needs to be in terms of M.

This version provides a constructive function f such that for all M ≥ 1 and N ≥ f(M), every maximal Sidon set A ⊆ {1,…,N} has another Sidon set B ⊆ {1,…,N} of size M with disjoint difference sets (apart from 0).

FormalConjectures/ErdosProblems/42.leanErdos42.erdos_42.variants.constructive6 linesExact file
sorry ↔  ∃ f,    ∀ (M N : ℕ),      1 ≤ M →        f M ≤ N →          ∀ (A : Set ℕ), A.IsMaximalSidonSetIn N → ∃ B ⊆ Set.Icc 1 N, IsSidon B ∧ B.ncard = M ∧ (A - A) ∩ (B - B) = {0}
OpenStatement only, no proof