Erdős Problem 329: Converse Implication
The converse: if the maximum density is 1, then any finite Sidon set can be embedded in a perfect difference set modulo .
Mathematical statement
The converse: if the maximum density is 1, then any finite Sidon set can be embedded in a perfect difference set modulo .
Since the consequent is false (due to the counterexamples in [Ha47] and [AlMi25]), this implication is logically equivalent to the statement that the maximum upper density of Sidon sets is NOT 1. Because the maximum upper density problem is still open, the truth value of this implication is also an open research problem.
Statement source: Erdős Problems statement material
Statement terms: Source-specific
Source-specific terms. Therefore does not assert reuse rights beyond attributed display.
Statement artifacts, not proofs
These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.
Pinned Lean formulation 1
erdos_329.variants.converse_implication
theorem erdos_329.variants.converse_implication : (sSup {sidonUpperDensity A | (A : Set ℕ) (_ : IsSidon A)} = 1) → (∀ (A : Finset ℕ), IsSidon (A : Set ℕ) → ∃ (D : Set ℕ) (n : ℕ) (_ : n > 0), ↑A ⊆ D ∧ IsPerfectDifferenceSet D n) := by sorry- Statement source
- Formal Conjectures
- Lean version
- v4.27.0
- Placeholder
- Present; no proof artifact
- Source evidence
- Pinned source index
- Fidelity review
- Community formulation
References