402.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

3 declarations, 3 contain sorry, 0 declared as axioms

Erdős Problem 402

Reference: erdosproblems.com/402

Imports (1)

FormalConjecturesUtil

theorem Erdos402.erdos_402 Prove that, for any finite set $A\subset\mathbb{N}$, there exist $a, b\in A$ such that $$ \gcd(a, b)\leq a/|A|. $$ sorry line 38 source
Source documentation
Prove that, for any finite set $A\subset\mathbb{N}$, there exist $a, b\in A$ such that $$ \gcd(a, b)\leq a/|A|. $$

depends on sorry what this means
Statement uses: Finset, Nat, Not, Membership.mem, OfNat.ofNat, Finset.Nonempty, Exists, And, LE.le, Rat, Nat.gcd, HDiv.hDiv, Finset.card
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_402 (A : Finset ℕ) (h₁ : 0 ∉ A) (h₂ : A.Nonempty) : ∃ᵉ (a ∈ A) (b ∈ A),
    a.gcd b ≤ (a / A.card : ℚ) := by
…
```
theorem Erdos402.erdos_402.variants.equality A conjecture of Graham [Gr70], who also conjectured that (assuming sorry line 53 source
Source documentation
A conjecture of Graham [Gr70], who also conjectured that (assuming $A$ itself has no common divisor) the only cases where equality is achieved are when $A = \{1, \dots, n\}$ or $A = \{L/1, \dots, L/n\}$ (where $L = \operatorname{lcm}(1, \dots, n)$) or $A = \{2, 3, 4, 6\}$. Note: The source [BaSo96] mentioned on the Erdős page makes it clear what quantifiers to use for "where equality is achieved". See Theorem 1.1 there.
TODO(firsching): Consider if we should have the other direction here as well or an iff statement.

depends on sorry what this means
Statement uses: Finset, Nat, Not, Membership.mem, OfNat.ofNat, Finset.Nonempty, Eq, Finset.gcd, id, LE.le, Rat, HDiv.hDiv, Finset.card, Nat.gcd, Or, Finset.Icc, Finset.image, Finset.lcm, Insert.insert, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
34 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_402.variants.equality (A : Finset ℕ) (h₁ : 0 ∉ A) (h₂ : A.Nonempty)
    (h₃ : A.gcd id = 1)
    (h : ∀ᵉ (a ∈ A) (b ∈ A), (a / A.card : ℚ) ≤ a.gcd b) :
    A = Finset.Icc 1 A.card ∨
    A = (Finset.Icc 1 A.card).image ((Finset.Icc 1 A.card).lcm id / ·) ∨
    A = {2, 3, 4, 6} := by
…
```
theorem Erdos402.erdos_402.variants.szegedy_zaharescu_weak Proved for all sufficiently large sets (including the sharper version which characterises the case of equality) independently by Szegedy [Sz86] and Zaharescu [Za87] sorry line 72 source
Source documentation
Proved for all sufficiently large sets (including the sharper version which characterises the case of equality) independently by Szegedy [Sz86] and Zaharescu [Za87]. The following is taken from [Sz86].
There exists an effectively computable $n_0$ with the following properties: (i) if $n \ge n_0$ and $a_1, a_2, \dots, a_n$ are distinct natural numbers then $\max_{i, j} \frac{a_i}{(a_i, a_j)} \ge n$. (ii) If equality holds then the system $\{a_1, a_2, \dots, a_n\}$ is either of the type $\{k, 2k, \dots, nk\}$ or of the type $\left\{\frac{k}{1}, \frac{k}{2}, \dots, \frac{k}{n}\right\}$.

depends on sorry what this means
Statement uses: Filter.Eventually, Nat, Finset, Eq, Finset.card, Not, Membership.mem, OfNat.ofNat, And, LE.le, Finset.sup, Prod, SProd.sprod, HDiv.hDiv, Prod.fst, Nat.gcd, Prod.snd, Iff, Exists, GT.gt and 7 more
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
38 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem erdos_402.variants.szegedy_zaharescu_weak : ∀ᶠ n in atTop,
    ∀ (A : Finset ℕ), A.card = n → 0 ∉ A →
      (n ≤ (A ×ˢ A).sup (fun x => x.1 / x.1.gcd x.2)) ∧
      (n = (A ×ˢ A).sup (fun x => x.1 / x.1.gcd x.2) ↔
        ∃ k > 0, A = (Finset.Icc 1 n).image (k * ·) ∨
          A = (Finset.Icc 1 n).image (k * (Finset.Icc 1 n).lcm id / ·)):= by
…
```