707.lean`

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

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

11 declarations, 8 contain sorry, 0 declared as axioms

Erdős Problem 707: Embedding Sidon Sets in Perfect Difference Sets

References:

erdosproblems.com/707
arxiv/2510.19804 Boris Alexeev and Dustin G. Mixon, Forbidden Sidon subsets of perfect difference sets, featuring a human-assisted proof (2025)
[Ha47] Marshall Hall, Jr., Cyclic projective planes, Duke Math. J. 14 (1947), 1079–1090.

Let A ⊆ ℕ be a finite Sidon set. Is there some set B with A ⊆ B which is a perfect difference set modulo p^2 + p + 1 for some prime power p?

This problem is related to Erdős Problem 329 about the maximum density of Sidon sets. If this conjecture is true, it would imply that the maximum density of Sidon sets is 1.

Imports (1)

FormalConjecturesUtil

theorem Erdos707.erdos_707 Erdős Problem 707: It is false that any finite Sidon set can be embedded in a perfect different set modulo some $n$ sorry line 53 source
Source documentation
Erdős Problem 707: It is false that any finite Sidon set can be embedded in a perfect different set modulo some $n$.
As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized.
This was formalized in Lean by Alexeev using ChatGPT.

depends on sorry what this means
Statement uses: Iff, Set, Nat, Set.Finite, IsSidon, Exists, And, GT.gt, OfNat.ofNat, LE.le, IsPerfectDifferenceSet, False
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707 : (∀ (A : Set ℕ) (h : A.Finite), IsSidon A →
    ∃ᵉ (B : Set ℕ) (n > 0), A ⊆ B ∧ IsPerfectDifferenceSet B n) ↔ False := by
…
```
Mentions: IsSidon, IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.prime_power It is false that any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime power p sorry line 66 source
Source documentation
It is false that any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime power p.
As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized.

depends on sorry what this means
Statement uses: Iff, Set, Nat, Set.Finite, IsSidon, Exists, And, IsPrimePow, LE.le, IsPerfectDifferenceSet, HAdd.hAdd, HPow.hPow, OfNat.ofNat, False
Proof uses: Eq.mpr, Not, id, Eq, Eq.trans, iff_false, congrArg, funext, forall_congr, implies_congr, Eq.refl, sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
24 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.prime_power : (∀ (A : Set ℕ) (h : A.Finite), IsSidon A →
    ∃ (B : Set ℕ) (p : ℕ), IsPrimePow p ∧ A ⊆ B ∧
    IsPerfectDifferenceSet B (p^2 + p + 1)) ↔ False := by
…
```
Mentions: IsSidon, IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.prime It is false that any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime p sorry line 80 source
Source documentation
It is false that any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime p.
As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized.

depends on sorry what this means
Statement uses: Iff, Set, Nat, Set.Finite, IsSidon, Exists, And, Nat.Prime, LE.le, IsPerfectDifferenceSet, HAdd.hAdd, HPow.hPow, OfNat.ofNat, False
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
18 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.prime : (∀ (A : Set ℕ) (h : A.Finite), IsSidon A →
    ∃ᵉ (B : Set ℕ) (p : ℕ), p.Prime ∧ A ⊆ B ∧ IsPerfectDifferenceSet B (p^2 + p + 1)) ↔ False := by
…
```
Mentions: IsSidon, IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.counterexample_prime Alexeev and Mixon [arxiv/2510.19804] have disproved this conjecture, proving that $\{1,2,4,8\}$ cannot be extended to a perfect difference set modulo $p^2+p+1$ for any prime $p$ sorry line 91 source
Source documentation
Alexeev and Mixon [arxiv/2510.19804] have disproved this conjecture, proving that $\{1,2,4,8\}$ cannot be extended to a perfect difference set modulo $p^2+p+1$ for any prime $p$.

depends on sorry what this means
Statement uses: Set, Nat, Eq, Insert.insert, OfNat.ofNat, Singleton.singleton, And, Finite, IsSidon, Prime, LE.le, Not, IsPerfectDifferenceSet, HAdd.hAdd, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
26 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.counterexample_prime (A : Set ℕ) (hA : A = {1, 2, 4, 8}) :
   Finite A ∧ IsSidon A ∧
   ∀ (B : Set ℕ) (p : ℕ),
    Prime p → A ⊆ B → ¬IsPerfectDifferenceSet B (p ^ 2 + p + 1) := by
…
```
Mentions: IsSidon, IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.counterexample_mian_chowla Alexeev and Mixon [arxiv/2510.19804] have disproved this conjecture, showing that $\{1, 2, 4, 8, 13\}$ cannot be extended to any perfect difference set modulo a positive integer sorry line 105 source
Source documentation
Alexeev and Mixon [arxiv/2510.19804] have disproved this conjecture, showing that $\{1, 2, 4, 8, 13\}$ cannot be extended to any perfect difference set modulo a positive integer. The modulus 0 is excluded, as in erdos_707: IsPerfectDifferenceSet B 0 describes an infinite perfect difference set in ℤ, and every finite Sidon set extends to one.

depends on sorry what this means
Statement uses: Set, Nat, Eq, Insert.insert, OfNat.ofNat, Singleton.singleton, And, Finite, IsSidon, LT.lt, LE.le, Not, IsPerfectDifferenceSet
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.counterexample_mian_chowla (A : Set ℕ) (hA : A = {1, 2, 4, 8, 13}) :
   Finite A ∧ IsSidon A ∧
   ∀ (B : Set ℕ) (n : ℕ), 0 < n → A ⊆ B → ¬IsPerfectDifferenceSet B n := by
…
```
Mentions: IsSidon, IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.counterexample_hall This conjecture was actually first disproved by Hall in 1947 [Ha47], long before Erdős asked this question sorry line 118 source
Source documentation
This conjecture was actually first disproved by Hall in 1947 [Ha47], long before Erdős asked this question. A counterexample for any modulus from from [Ha47] in the paragraph following Theorem 4.3, where it was given as $\{-8, -6, 0, 1, 4\}$, but this can be shifted to natural numbers as pointed out in [arxiv/2510.19804].

depends on sorry what this means
Statement uses: Set, Nat, Eq, Insert.insert, OfNat.ofNat, Singleton.singleton, And, Finite, IsSidon, LT.lt, LE.le, Not, IsPerfectDifferenceSet
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.counterexample_hall (A : Set ℕ) (hA : A = {1, 3, 9, 10, 13}) :
   Finite A ∧ IsSidon A ∧
   ∀ (B : Set ℕ) (n : ℕ), 0 < n → A ⊆ B → ¬IsPerfectDifferenceSet B n := by
…
```
Mentions: IsSidon, IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.perfect_difference_set_size_bound A perfect difference set modulo n must have size ≤ √n + 1 line 130 source
Source documentation
A perfect difference set modulo n must have size ≤ √n + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Nat, IsPerfectDifferenceSet, LE.le, Set.ncard, HAdd.hAdd, Nat.sqrt, OfNat.ofNat
Proof uses: dite, Set.Finite, Classical.propDecidable, Eq, Eq.mpr, id, congrArg, Eq.trans, congrFun', Nat.sqrt_zero, zero_add, Decidable.byContradiction, Not, Set.Finite.not_infinite, ZMod, Set.ofPred, Ne, Set.Finite.subset, Set.image, Prod and 119 more
129 instances, coercions and auxiliary constants left out.

Tactic trace: 32 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.perfect_difference_set_size_bound (B : Set ℕ) (n : ℕ)
    (hB : IsPerfectDifferenceSet B n) : B.ncard ≤ n.sqrt + 1 := by
…
```
Mentions: IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.singer_construction The Singer construction gives perfect difference sets for n = p^2 + p + 1 where p is a prime power sorry line 163 source
Source documentation
The Singer construction gives perfect difference sets for n = p^2 + p + 1 where p is a prime power.

depends on sorry what this means
Statement uses: Nat, IsPrimePow, Exists, Set, And, IsPerfectDifferenceSet, HAdd.hAdd, HPow.hPow, OfNat.ofNat, Eq, Set.ncard
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.singer_construction (p : ℕ) (hp : IsPrimePow p) :
    ∃ (B : Set ℕ), IsPerfectDifferenceSet B (p^2 + p + 1) ∧ B.ncard = p + 1 := by
…
```
Mentions: IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.example_sidon_set The set {1, 2, 4} is a Sidon set line 173 source
Source documentation
The set {1, 2, 4} is a Sidon set.

standard axioms: propext what this means
Statement uses: IsSidon, Nat, Insert.insert, Set, OfNat.ofNat, Singleton.singleton
Proof uses: Membership.mem, Eq, HAdd.hAdd, Or, And, Eq.mp, Eq.trans, congrArg, of_eq_true, True, congr, eq_self, and_self, or_self, Eq.symm, False.elim, False, eq_false_of_decide, Eq.refl, Bool and 3 more
25 instances, coercions and auxiliary constants left out.

Tactic trace: 7 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.example_sidon_set : IsSidon ({1, 2, 4} : Set ℕ) := by
…
```
Mentions: IsSidon
theorem Erdos707.erdos_707.variants.example_embedding The set {1, 2, 4} can be embedded in a perfect difference set modulo 7 line 186 source
Source documentation
The set {1, 2, 4} can be embedded in a perfect difference set modulo 7.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Exists, Set, Nat, And, LE.le, Insert.insert, OfNat.ofNat, Singleton.singleton, IsPerfectDifferenceSet
Proof uses: Exists.intro, And.intro, Set.Subset.refl, id, Set.MapsTo, Prod, ZMod, IsPerfectDifferenceSet.match_1, HSub.hSub, Set.offDiag, Set.ofPred, Ne, Set.InjOn, Set.SurjOn, Membership.mem, Prod.mk, Or, Eq, Eq.mp, Eq.trans and 51 more
55 instances, coercions and auxiliary constants left out.

Tactic trace: 52 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.example_embedding : ∃ (B : Set ℕ), {1, 2, 4} ⊆ B ∧
    IsPerfectDifferenceSet B 7 := by
…
```
Mentions: IsPerfectDifferenceSet
theorem Erdos707.erdos_707.variants.small_sidon_sets For small Sidon sets, we can check the conjecture directly sorry line 220 source
Source documentation
For small Sidon sets, we can check the conjecture directly.

depends on sorry what this means
Statement uses: Set, Nat, Set.Finite, LE.le, Set.ncard, OfNat.ofNat, IsSidon, Exists, And, IsPrimePow, IsPerfectDifferenceSet, HAdd.hAdd, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
22 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_707.variants.small_sidon_sets (A : Set ℕ) (hA : A.Finite) (h : A.ncard ≤ 3)
    (hSidon : IsSidon A) : ∃ (B : Set ℕ) (p : ℕ), IsPrimePow p ∧ A ⊆ B ∧
    IsPerfectDifferenceSet B (p^2 + p + 1) := by
…
```
Mentions: IsSidon, IsPerfectDifferenceSet

FormalConjectures/ErdosProblems/707.lean

Erdős Problem 707: Embedding Sidon Sets in Perfect Difference Sets

As described in [arxiv/2510.19804], a counterexample is provided in [Ha47], see below. The proof of this has been formalized.

`FormalConjectures/ErdosProblems/707.lean`