FormalConjectures/ErdosProblems/42.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

5 declarations, 2 contain sorry, 0 declared as axioms

Erdős Problem 42: Maximal Sidon Sets and Disjoint Difference Sets

Reference: erdosproblems.com/42

This problem asks whether maximal Sidon sets can coexist with other Sidon sets that have disjoint difference sets (apart from 0).

Imports (1)
Imported by 1 file
  1. theorem Erdos42.erdos_42 Erdős Problem 42: Let M ≥ 1 and N be sufficiently large in terms of M sorry line 44 source

    Source documentation

    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}?

    This was proved for all $M$ by GPT 5.5 Pro (prompted by Sandhu), see discussion thread for more details.

    depends on sorry what this means

    Statement uses: Iff, True, Nat, GE.ge, OfNat.ofNat, Filter.Eventually, Set, Set.IsMaximalSidonSetIn, Exists, And, LE.le, Set.Icc, IsSidon, Eq, Set.ncard, Inter.inter, HSub.hSub, Singleton.singleton, Filter.atTop

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

    theorem erdos_42 : answer(True) ↔
    ∀ M ≥ 1, ∀ᶠ N in atTop, ∀ (A : Set ℕ) (_ : IsMaximalSidonSetIn A N),
    ∃ᵉ (B : Set ℕ), B ⊆ Set.Icc 1 N ∧ IsSidon B ∧ B.ncard = M ∧
    ((A - A) ∩ (B - B)) = {0} := by
…

    Mentions: IsSidon

  2. theorem Erdos42.erdos_42.variants.constructive sorry line 59 source

    depends on sorry what this means

    Statement uses: Iff, True, Exists, Nat, LE.le, OfNat.ofNat, Set, Set.IsMaximalSidonSetIn, And, Set.Icc, IsSidon, Eq, Set.ncard, Inter.inter, HSub.hSub, Singleton.singleton

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    20 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. theorem Erdos42.example_maximal_sidon The set {1, 2, 4} is a maximal Sidon set in {1, ..., 4} line 73 source

    Source documentation

    The set {1, 2, 4} is a maximal Sidon set in {1, ..., 4}.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Set.IsMaximalSidonSetIn, Insert.insert, Nat, Set, OfNat.ofNat, Singleton.singleton

    Proof uses: And.intro, LE.le, Set.Icc, And, IsSidon, Membership.mem, Not, Union.union, Eq, Or, Eq.mp, Eq.trans, congrArg, of_eq_true, True, congr, and_self, Eq.symm, eq_true_of_decide, Eq.refl and 17 more

    47 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

    Open to load the checked before-and-after goal states.

    theorem example_maximal_sidon : IsMaximalSidonSetIn {1, 2, 4} 4 := by
…
  4. theorem Erdos42.example_difference_set The difference set of {1, 2, 4} is {0, 1, 2, 3} line 98 source

    Source documentation

    The difference set of {1, 2, 4} is {0, 1, 2, 3}.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Eq, Set, Nat, HSub.hSub, Insert.insert, OfNat.ofNat, Singleton.singleton

    Proof uses: Set.ext, Eq.mpr, Iff, Membership.mem, Exists, And, Or, id, congr, congrArg, Eq.trans, funext, congrFun', Iff.intro, of_eq_true, True, False, tsub_self, eq_self, or_self and 15 more

    58 instances, coercions and auxiliary constants left out.

    Tactic trace: 30 steps

    Open to load the checked before-and-after goal states.

    theorem example_difference_set : ({1, 2, 4} : Set ℕ) - {1, 2, 4} = {0, 1, 2, 3} := by
…
  5. theorem Erdos42.maximal_sidon_contains_zero For any maximal Sidon set, the difference set contains 0 line 116 source

    Source documentation

    For any maximal Sidon set, the difference set contains 0.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Set, Nat, LE.le, OfNat.ofNat, Set.IsMaximalSidonSetIn, Membership.mem, HSub.hSub

    Proof uses: Set.Icc, And, IsSidon, Not, Union.union, Singleton.singleton, Set.Nonempty, Classical.byContradiction, Iff.mpr, Set.mem_Icc, And.intro, le_refl, Eq.mpr, EmptyCollection.emptyCollection, id, Eq, congrArg, Eq.mp, propext, Set.not_nonempty_iff_eq_empty and 8 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

    Open to load the checked before-and-after goal states.

    theorem maximal_sidon_contains_zero (A : Set ℕ) (N : ℕ) (hN : 1 ≤ N)
    (hA : IsMaximalSidonSetIn A N) : 0 ∈ A - A := by
…