Erdős problem 42
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}?
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/42.leanTrue ↔ ∀ 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}Proof manifests naming this Problem
- Jayyhk Erdős Lean
jayyhk:erdos:42 - PLBY Lean proofs
ErdosProblems.Erdos42
Reported activity
Work these sources record against this Problem. Source-reported attribution, not reviewed here.
AI standalone
- Machine
AI collaborating with humans
- Machine
- People
Formalization
- Machine
argument
- Machine
- People
- Reported outcome