Open Proof Network

Problems / erdos-402 / variant-b89de5c4

Graham's bound for |A| = 18

variant-b89de5c4

proved

A partial route to the problem.

$\displaystyle \forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 18 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

Every set A of exactly eighteen positive integers has a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

unverified · history

Lean
theorem Opn.erdos_402_card_eighteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 18 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  sorry
Why does it end in sorry?

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

How it was proved

Proved by Proof.lean, checked by the kernel. Its attestation, 000279, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000279.json, merge commit 423883f8a194.

Outline of Proof.lean, extracted by the gate at 82834c4684b8 from the proof’s elaboration: each step is a claim the proof establishes and the goal it leaves. Open a step for what it uses and its Lean lines.

  1. red have ∀ (n L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ), (2 : ℕ) ≤ n → (0 : ℕ) < L → (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, (0 : ℕ) < j → k ∣ L * j ∧ L * j / k ∈ S) → (∀ a ∈ S, c a + (2 : ℕ) < n) → (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) → ∀ (A : Finset ℕ), (0 : ℕ) ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with red : ∀ (n L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ), (2 : ℕ) ≤ n → (0 : ℕ) < L → (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, (0 : ℕ) < j → k ∣ L * j ∧ L * j / k ∈ S) → (∀ a ∈ S, c a + (2 : ℕ) < n) → (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) → ∀ (A : Finset ℕ), (0 : ℕ) ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

    Uses library Finset Finset α is the type of finite sets of elements of α. , Finset.range range n is the set of natural numbers less than n. , Nat.mul_div_cancel.

    Lean, lines 13–111
      have red :
      ∀ (n L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ), 2 ≤ n → 0 < L →
        (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, 0 < j → k ∣ L * j ∧ L * j / k ∈ S) →
        (∀ a ∈ S, c a + 2 < n) →
        (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) →
        ∀ A : Finset ℕ, 0 ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
    intro n L S c hn hL hS hc hgood A hA hcard
    have hpos : 0 < A.card := by omega
    have hne : A.Nonempty := Finset.card_pos.mp hpos
    have key : ∀ a b : ℕ, a.gcd b * A.card ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
      intro a b h
      rw [le_div_iff₀ (by exact_mod_cast hpos)]
      exact_mod_cast h
    have hM : A.max' hne ∈ A := Finset.max'_mem A hne
    have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))
    by_cases hw : ∃ x ∈ A, (A.max' hne).gcd x * n ≤ A.max' hne
    · obtain ⟨x, hx, h⟩ := hw
      exact ⟨_, hM, x, hx, key _ x (by rw [hcard]; exact h)⟩
    push_neg at hw
    have forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne := by
      intro x hx
      rw [Finset.mem_erase] at hx
      obtain ⟨hxM, hxA⟩ := hx
      have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))
      have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
      have hg := hw x hxA
      have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
      obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
      obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
      have hj1 : 0 < j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · rw [h, Nat.mul_zero] at hj
          omega
        · exact h
      have hjk : j < k := by
        have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
          rw [← hj, ← hk]
          exact hlt
        exact Nat.lt_of_mul_lt_mul_left h1
      have hkn : k < n := by
        have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
          rw [← hk]
          exact hg
        exact Nat.lt_of_mul_lt_mul_left h1
      have hkx : k * x = j * A.max' hne := by
        calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
          _ = j * ((A.max' hne).gcd x * k) := by ring
          _ = j * A.max' hne := by rw [← hk]
      have hkpos : 0 < k := by omega
      obtain ⟨hdvd, hmem⟩ := hS k (Finset.mem_range.2 hkn) j (Finset.mem_range.2 hjk) hj1
      obtain ⟨q, hq⟩ := hdvd
      refine ⟨L * j / k, hmem, ?_⟩
      rw [hq, Nat.mul_div_cancel_left q hkpos]
      apply Nat.eq_of_mul_eq_mul_left hkpos
      calc k * (L * x) = L * (k * x) := by ring
        _ = L * (j * A.max' hne) := by rw [hkx]
        _ = (L * j) * A.max' hne := by ring
        _ = (k * q) * A.max' hne := by rw [hq]
        _ = k * (q * A.max' hne) := by ring
    have hmaps : ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - 2) := by
      intro x hx
      obtain ⟨a, ha, hax⟩ := forms x hx
      rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
      have := hc a ha
      omega
    have hcardE : (A.erase (A.max' hne)).card = n - 1 := by
      rw [Finset.card_erase_of_mem hM, hcard]
    obtain ⟨x, hx, y, hy, hxy, hcol⟩ :=
      Finset.exists_ne_map_eq_of_card_lt_of_maps_to
        (by rw [hcardE, Finset.card_range]; omega) hmaps
    obtain ⟨a, ha, hax⟩ := forms x hx
    obtain ⟨b, hb, hby⟩ := forms y hy
    rw [hax, hby, Nat.mul_div_cancel _ hMpos, Nat.mul_div_cancel _ hMpos] at hcol
    have hab : a ≠ b := by
      intro h
      apply hxy
      apply Nat.eq_of_mul_eq_mul_left hL
      rw [hax, hby, h]
    have hgcd : a.gcd b * A.max' hne = L * x.gcd y := by
      have h1 : Nat.gcd (L * x) (L * y) = L * x.gcd y := Nat.gcd_mul_left L x y
      rw [hax, hby, Nat.gcd_mul_right] at h1
      exact h1
    have hxA := (Finset.mem_erase.mp hx).2
    have hyA := (Finset.mem_erase.mp hy).2
    rcases hgood a ha b hb hab hcol with h | h
    · refine ⟨x, hxA, y, hyA, key x y ?_⟩
      rw [hcard]
      have h2 : L * (x.gcd y * n) ≤ L * x := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * x := hax.symm
      exact Nat.le_of_mul_le_mul_left h2 hL
    · refine ⟨y, hyA, x, hxA, key y x ?_⟩
      rw [hcard, Nat.gcd_comm]
      have h2 : L * (x.gcd y * n) ≤ L * y := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * y := hby.symm
      exact Nat.le_of_mul_le_mul_left h2 hL

    targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 13–111 at 423883f8a194 ↗

    1. red.hpos have (0 : ℕ) < A.card routine: omega

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hpos : (0 : ℕ) < A.card.

      Lean, line 20
          have hpos : 0 < A.card := by omega

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 20 at 423883f8a194 ↗

    2. red.hne have A.Nonempty

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hne : A.Nonempty.

      Uses library Finset.card_pos.

      Lean, line 21
          have hne : A.Nonempty := Finset.card_pos.mp hpos

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 21 at 423883f8a194 ↗

    3. red.key have ∀ (a b : ℕ), a.gcd b * A.card ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with key : ∀ (a b : ℕ), a.gcd b * A.card ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

      Uses library le_div_iff₀ See le_div_iff₀' for a version with multiplication on the other side. .

      Lean, lines 22–25
          have key : ∀ a b : ℕ, a.gcd b * A.card ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
      intro a b h
      rw [le_div_iff₀ (by exact_mod_cast hpos)]
      exact_mod_cast h

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 22–25 at 423883f8a194 ↗

    4. red.hM have A.max' hne ∈ A

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hM : A.max' hne ∈ A.

      Uses library Finset.max'_mem.

      Lean, line 26
          have hM : A.max' hne ∈ A := Finset.max'_mem A hne

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 26 at 423883f8a194 ↗

    5. red.hMpos have (0 : ℕ) < A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hMpos : (0 : ℕ) < A.max' hne.

      Uses library Nat.pos_of_ne_zero.

      Lean, line 27
          have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 27 at 423883f8a194 ↗

    6. red.s6 case

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

      Uses library Exists.intro Existential introduction. .

      Lean, lines 29–30
          · obtain ⟨x, hx, h⟩ := hw
      exact ⟨_, hM, x, hx, key _ x (by rw [hcard]; exact h)⟩

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 29–30 at 423883f8a194 ↗

      1. red.s6.s1 obtain ∃ x ∈ A, (A.max' hne).gcd x * n ≤ A.max' hne

        Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A, h : (A.max' hne).gcd x * n ≤ A.max' hne.

        Lean, line 29
            · obtain ⟨x, hx, h⟩ := hw

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 29 at 423883f8a194 ↗

    7. red.forms have ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne.

      Uses library Finset.mem_erase, Exists.intro Existential introduction. , Nat.mul_div_cancel_left, Nat.eq_of_mul_eq_mul_left.

      Lean, lines 32–71
          have forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne := by
      intro x hx
      rw [Finset.mem_erase] at hx
      obtain ⟨hxM, hxA⟩ := hx
      have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))
      have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
      have hg := hw x hxA
      have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
      obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
      obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
      have hj1 : 0 < j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · rw [h, Nat.mul_zero] at hj
          omega
        · exact h
      have hjk : j < k := by
        have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
          rw [← hj, ← hk]
          exact hlt
        exact Nat.lt_of_mul_lt_mul_left h1
      have hkn : k < n := by
        have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
          rw [← hk]
          exact hg
        exact Nat.lt_of_mul_lt_mul_left h1
      have hkx : k * x = j * A.max' hne := by
        calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
          _ = j * ((A.max' hne).gcd x * k) := by ring
          _ = j * A.max' hne := by rw [← hk]
      have hkpos : 0 < k := by omega
      obtain ⟨hdvd, hmem⟩ := hS k (Finset.mem_range.2 hkn) j (Finset.mem_range.2 hjk) hj1
      obtain ⟨q, hq⟩ := hdvd
      refine ⟨L * j / k, hmem, ?_⟩
      rw [hq, Nat.mul_div_cancel_left q hkpos]
      apply Nat.eq_of_mul_eq_mul_left hkpos
      calc k * (L * x) = L * (k * x) := by ring
        _ = L * (j * A.max' hne) := by rw [hkx]
        _ = (L * j) * A.max' hne := by ring
        _ = (k * q) * A.max' hne := by rw [hq]
        _ = k * (q * A.max' hne) := by ring

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 32–71 at 423883f8a194 ↗

      1. red.forms.s1 obtain x ≠ A.max' hne ∧ x ∈ A

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hxM : x ≠ A.max' hne, hxA : x ∈ A.

        Lean, line 35
              obtain ⟨hxM, hxA⟩ := hx

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 35 at 423883f8a194 ↗

      2. red.forms.hxpos have (0 : ℕ) < x

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hxpos : (0 : ℕ) < x.

        Uses library Nat.pos_of_ne_zero.

        Lean, line 36
              have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 36 at 423883f8a194 ↗

      3. red.forms.hlt have x < A.max' hne

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hlt : x < A.max' hne.

        Uses library lt_of_le_of_ne, Finset.le_max'.

        Lean, line 37
              have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 37 at 423883f8a194 ↗

      4. red.forms.hg have A.max' hne < (A.max' hne).gcd x * n

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hg : A.max' hne < (A.max' hne).gcd x * n.

        Lean, line 38
              have hg := hw x hxA

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 38 at 423883f8a194 ↗

      5. red.forms.hgpos have (0 : ℕ) < (A.max' hne).gcd x

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hgpos : (0 : ℕ) < (A.max' hne).gcd x.

        Uses library Nat.gcd_pos_of_pos_right.

        Lean, line 39
              have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 39 at 423883f8a194 ↗

      6. red.forms.s6 obtain (A.max' hne).gcd x ∣ A.max' hne

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with k : ℕ, hk : A.max' hne = (A.max' hne).gcd x * k.

        Uses library Nat.gcd_dvd_left.

        Lean, line 40
              obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 40 at 423883f8a194 ↗

      7. red.forms.s7 obtain (A.max' hne).gcd x ∣ x

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with j : ℕ, hj : x = (A.max' hne).gcd x * j.

        Uses library Nat.gcd_dvd_right.

        Lean, line 41
              obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 41 at 423883f8a194 ↗

      8. red.forms.hj1 have (0 : ℕ) < j

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hj1 : (0 : ℕ) < j.

        Uses library Nat.eq_zero_or_pos.

        Lean, lines 42–46
              have hj1 : 0 < j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · rw [h, Nat.mul_zero] at hj
          omega
        · exact h

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 42–46 at 423883f8a194 ↗

        1. red.forms.hj1.s1 case

          Leaves (0 : ℕ) < j.

          Uses library Nat.mul_zero.

          Lean, lines 44–45
                  · rw [h, Nat.mul_zero] at hj
          omega

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 44–45 at 423883f8a194 ↗

        2. red.forms.hj1.s2 case

          Leaves (0 : ℕ) < j.

          Lean, line 46
                  · exact h

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 46 at 423883f8a194 ↗

      9. red.forms.hjk have j < k

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hjk : j < k.

        Uses library Nat.lt_of_mul_lt_mul_left.

        Lean, lines 47–51
              have hjk : j < k := by
        have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
          rw [← hj, ← hk]
          exact hlt
        exact Nat.lt_of_mul_lt_mul_left h1

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 47–51 at 423883f8a194 ↗

        1. red.forms.hjk.h1 have (A.max' hne).gcd x * j < (A.max' hne).gcd x * k

          Leaves j < k, with h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k.

          Lean, lines 48–50
                  have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
          rw [← hj, ← hk]
          exact hlt

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 48–50 at 423883f8a194 ↗

      10. red.forms.hkn have k < n

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hkn : k < n.

        Uses library Nat.lt_of_mul_lt_mul_left.

        Lean, lines 52–56
              have hkn : k < n := by
        have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
          rw [← hk]
          exact hg
        exact Nat.lt_of_mul_lt_mul_left h1

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 52–56 at 423883f8a194 ↗

        1. red.forms.hkn.h1 have (A.max' hne).gcd x * k < (A.max' hne).gcd x * n

          Leaves k < n, with h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n.

          Lean, lines 53–55
                  have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
          rw [← hk]
          exact hg

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 53–55 at 423883f8a194 ↗

      11. red.forms.hkx have k * x = j * A.max' hne

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hkx : k * x = j * A.max' hne.

        Lean, lines 57–60
              have hkx : k * x = j * A.max' hne := by
        calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
          _ = j * ((A.max' hne).gcd x * k) := by ring
          _ = j * A.max' hne := by rw [← hk]

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 57–60 at 423883f8a194 ↗

        1. red.forms.hkx.s1 calc k * x = k * ((A.max' hne).gcd x * j)

          Closes the goal.

          Lean, line 58
                  calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 58 at 423883f8a194 ↗

        2. red.forms.hkx.s2 calc routine: ring

          Closes the goal.

          Lean, line 59
                    _ = j * ((A.max' hne).gcd x * k) := by ring

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 59 at 423883f8a194 ↗

        3. red.forms.hkx.s3 calc

          Closes the goal.

          Lean, line 60
                    _ = j * A.max' hne := by rw [← hk]

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 60 at 423883f8a194 ↗

      12. red.forms.hkpos have (0 : ℕ) < k routine: omega

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hkpos : (0 : ℕ) < k.

        Lean, line 61
              have hkpos : 0 < k := by omega

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 61 at 423883f8a194 ↗

      13. red.forms.s13 obtain k ∣ L * j ∧ L * j / k ∈ S

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hdvd : k ∣ L * j, hmem : L * j / k ∈ S.

        Uses library Finset.mem_range.

        Lean, line 62
              obtain ⟨hdvd, hmem⟩ := hS k (Finset.mem_range.2 hkn) j (Finset.mem_range.2 hjk) hj1

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 62 at 423883f8a194 ↗

      14. red.forms.s14 obtain k ∣ L * j

        Leaves ∃ a ∈ S, L * x = a * A.max' hne, with q : ℕ, hq : L * j = k * q.

        Lean, line 63
              obtain ⟨q, hq⟩ := hdvd

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 63 at 423883f8a194 ↗

      15. red.forms.s15 calc k * (L * x) = L * (k * x) routine: ring

        Closes the goal.

        Lean, line 67
              calc k * (L * x) = L * (k * x) := by ring

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 67 at 423883f8a194 ↗

      16. red.forms.s16 calc

        Closes the goal.

        Lean, line 68
                _ = L * (j * A.max' hne) := by rw [hkx]

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 68 at 423883f8a194 ↗

      17. red.forms.s17 calc routine: ring

        Closes the goal.

        Lean, line 69
                _ = (L * j) * A.max' hne := by ring

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 69 at 423883f8a194 ↗

      18. red.forms.s18 calc

        Closes the goal.

        Lean, line 70
                _ = (k * q) * A.max' hne := by rw [hq]

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 70 at 423883f8a194 ↗

      19. red.forms.s19 calc routine: ring

        Closes the goal.

        Lean, line 71
                _ = k * (q * A.max' hne) := by ring

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 71 at 423883f8a194 ↗

    8. red.hmaps have ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - (2 : ℕ))

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - (2 : ℕ)).

      Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mem_range, Nat.mul_div_cancel.

      Lean, lines 72–77
          have hmaps : ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - 2) := by
      intro x hx
      obtain ⟨a, ha, hax⟩ := forms x hx
      rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
      have := hc a ha
      omega

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 72–77 at 423883f8a194 ↗

      1. red.hmaps.s1 obtain ∃ a ∈ S, L * x = a * A.max' hne

        Leaves c (L * x / A.max' hne) ∈ Finset.range (n - (2 : ℕ)), with a : ℕ, ha : a ∈ S, hax : L * x = a * A.max' hne.

        Lean, line 74
              obtain ⟨a, ha, hax⟩ := forms x hx

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 74 at 423883f8a194 ↗

      2. red.hmaps.this have c a + (2 : ℕ) < n

        Leaves c a < n - (2 : ℕ), with this : c a + (2 : ℕ) < n.

        Lean, line 76
              have := hc a ha

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 76 at 423883f8a194 ↗

    9. red.hcardE have (A.erase (A.max' hne)).card = n - (1 : ℕ)

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcardE : (A.erase (A.max' hne)).card = n - (1 : ℕ).

      Uses library Finset.card_erase_of_mem $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. .

      Lean, lines 78–79
          have hcardE : (A.erase (A.max' hne)).card = n - 1 := by
      rw [Finset.card_erase_of_mem hM, hcard]

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 78–79 at 423883f8a194 ↗

    10. red.s10 obtain ∃ x ∈ A.erase (A.max' hne), ∃ y ∈ A.erase (A.max' hne), x ≠ y ∧ c (L * x / A.max' hne) = c (L * y / A.max' hne)

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A.erase (A.max' hne), y : ℕ, hy : y ∈ A.erase (A.max' hne), hxy : x ≠ y, hcol : c (L * x / A.max' hne) = c (L * y / A.max' hne).

      Uses library Finset.exists_ne_map_eq_of_card_lt_of_maps_to If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole. , Finset.card_range.

      Lean, lines 80–82
          obtain ⟨x, hx, y, hy, hxy, hcol⟩ :=
      Finset.exists_ne_map_eq_of_card_lt_of_maps_to
        (by rw [hcardE, Finset.card_range]; omega) hmaps

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 80–82 at 423883f8a194 ↗

    11. red.s11 obtain ∃ a ∈ S, L * x = a * A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with a : ℕ, ha : a ∈ S, hax : L * x = a * A.max' hne.

      Lean, line 83
          obtain ⟨a, ha, hax⟩ := forms x hx

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 83 at 423883f8a194 ↗

    12. red.s12 obtain ∃ a ∈ S, L * y = a * A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with b : ℕ, hb : b ∈ S, hby : L * y = b * A.max' hne.

      Lean, line 84
          obtain ⟨b, hb, hby⟩ := forms y hy

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 84 at 423883f8a194 ↗

    13. red.hab have a ≠ b

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hab : a ≠ b.

      Uses library Nat.eq_of_mul_eq_mul_left.

      Lean, lines 86–90
          have hab : a ≠ b := by
      intro h
      apply hxy
      apply Nat.eq_of_mul_eq_mul_left hL
      rw [hax, hby, h]

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 86–90 at 423883f8a194 ↗

    14. red.hgcd have a.gcd b * A.max' hne = L * x.gcd y

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgcd : a.gcd b * A.max' hne = L * x.gcd y.

      Uses library Nat.gcd_mul_right.

      Lean, lines 91–94
          have hgcd : a.gcd b * A.max' hne = L * x.gcd y := by
      have h1 : Nat.gcd (L * x) (L * y) = L * x.gcd y := Nat.gcd_mul_left L x y
      rw [hax, hby, Nat.gcd_mul_right] at h1
      exact h1

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 91–94 at 423883f8a194 ↗

      1. red.hgcd.h1 have (L * x).gcd (L * y) = L * x.gcd y

        Leaves a.gcd b * A.max' hne = L * x.gcd y, with h1 : (L * x).gcd (L * y) = L * x.gcd y.

        Uses library Nat.gcd Computes the greatest common divisor of two natural numbers. , Nat.gcd_mul_left.

        Lean, line 92
              have h1 : Nat.gcd (L * x) (L * y) = L * x.gcd y := Nat.gcd_mul_left L x y

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 92 at 423883f8a194 ↗

    15. red.hxA have x ∈ A

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hxA : x ∈ A.

      Uses library Finset.mem_erase.

      Lean, line 95
          have hxA := (Finset.mem_erase.mp hx).2

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 95 at 423883f8a194 ↗

    16. red.hyA have y ∈ A

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hyA : y ∈ A.

      Uses library Finset.mem_erase.

      Lean, line 96
          have hyA := (Finset.mem_erase.mp hy).2

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 96 at 423883f8a194 ↗

    17. red.s17 case

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

      Uses library Exists.intro Existential introduction. , Nat.le_of_mul_le_mul_left.

      Lean, lines 98–104
          · refine ⟨x, hxA, y, hyA, key x y ?_⟩
      rw [hcard]
      have h2 : L * (x.gcd y * n) ≤ L * x := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * x := hax.symm
      exact Nat.le_of_mul_le_mul_left h2 hL

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 98–104 at 423883f8a194 ↗

      1. red.s17.h2 have L * (x.gcd y * n) ≤ L * x

        Leaves x.gcd y * n ≤ x, with h2 : L * (x.gcd y * n) ≤ L * x.

        Lean, lines 100–103
              have h2 : L * (x.gcd y * n) ≤ L * x := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * x := hax.symm

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 100–103 at 423883f8a194 ↗

        1. red.s17.h2.s1 calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne)

          Closes the goal.

          Lean, line 101
                  calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 101 at 423883f8a194 ↗

        2. red.s17.h2.s2 calc n * (a.gcd b * A.max' hne) ≤ a * A.max' hne

          Closes the goal.

          Uses library Nat.mul_le_mul_right.

          Lean, line 102
                    _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 102 at 423883f8a194 ↗

        3. red.s17.h2.s3 calc a * A.max' hne = L * x

          Closes the goal.

          Lean, line 103
                    _ = L * x := hax.symm

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 103 at 423883f8a194 ↗

    18. red.s18 case

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).

      Uses library Exists.intro Existential introduction. , Nat.gcd_comm, Nat.le_of_mul_le_mul_left.

      Lean, lines 105–111
          · refine ⟨y, hyA, x, hxA, key y x ?_⟩
      rw [hcard, Nat.gcd_comm]
      have h2 : L * (x.gcd y * n) ≤ L * y := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * y := hby.symm
      exact Nat.le_of_mul_le_mul_left h2 hL

      targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 105–111 at 423883f8a194 ↗

      1. red.s18.h2 have L * (x.gcd y * n) ≤ L * y

        Leaves x.gcd y * n ≤ y, with h2 : L * (x.gcd y * n) ≤ L * y.

        Lean, lines 107–110
              have h2 : L * (x.gcd y * n) ≤ L * y := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * y := hby.symm

        targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, lines 107–110 at 423883f8a194 ↗

        1. red.s18.h2.s1 calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne)

          Closes the goal.

          Lean, line 108
                  calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 108 at 423883f8a194 ↗

        2. red.s18.h2.s2 calc n * (a.gcd b * A.max' hne) ≤ b * A.max' hne

          Closes the goal.

          Uses library Nat.mul_le_mul_right.

          Lean, line 109
                    _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 109 at 423883f8a194 ↗

        3. red.s18.h2.s3 calc b * A.max' hne = L * y

          Closes the goal.

          Lean, line 110
                    _ = L * y := hby.symm

          targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, line 110 at 423883f8a194 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000279.json, merge commit 423883f8a194.

Proof.lean — its sha256 is the artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-402/nodes/variant-b89de5c4/Proof.lean, sha256 3f0cf8cdfa55.
import Mathlib
import Nodes.«variant-b89de5c4».Context

/-! Graham's gcd conjecture (Erdős problem 402) for eighteen-element sets. With M the largest
element, if gcd(M, x) > M/18 for every x then every other x is (j/k)M with j < k ≤ 17, so
L·x/M (L = lcm(1..17) = 12252240) lies in a fixed set S of 95 values. S splits into 16 classes in
each of which any two distinct values c, d have 18·gcd(c, d) ≤ c or ≤ d; by pigeonhole two of
the 17 other elements share a class, and gcd(x, y)·L = gcd(c, d)·M transfers the bound. -/

theorem Opn.erdos_402_card_eighteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 18 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A hA hn
  have red :
      ∀ (n L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ), 2 ≤ n → 0 < L →
        (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, 0 < j → k ∣ L * j ∧ L * j / k ∈ S) →
        (∀ a ∈ S, c a + 2 < n) →
        (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) →
        ∀ A : Finset ℕ, 0 ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
    intro n L S c hn hL hS hc hgood A hA hcard
    have hpos : 0 < A.card := by omega
    have hne : A.Nonempty := Finset.card_pos.mp hpos
    have key : ∀ a b : ℕ, a.gcd b * A.card ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
      intro a b h
      rw [le_div_iff₀ (by exact_mod_cast hpos)]
      exact_mod_cast h
    have hM : A.max' hne ∈ A := Finset.max'_mem A hne
    have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))
    by_cases hw : ∃ x ∈ A, (A.max' hne).gcd x * n ≤ A.max' hne
    · obtain ⟨x, hx, h⟩ := hw
      exact ⟨_, hM, x, hx, key _ x (by rw [hcard]; exact h)⟩
    push_neg at hw
    have forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne := by
      intro x hx
      rw [Finset.mem_erase] at hx
      obtain ⟨hxM, hxA⟩ := hx
      have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))
      have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
      have hg := hw x hxA
      have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
      obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
      obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
      have hj1 : 0 < j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · rw [h, Nat.mul_zero] at hj
          omega
        · exact h
      have hjk : j < k := by
        have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
          rw [← hj, ← hk]
          exact hlt
        exact Nat.lt_of_mul_lt_mul_left h1
      have hkn : k < n := by
        have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
          rw [← hk]
          exact hg
        exact Nat.lt_of_mul_lt_mul_left h1
      have hkx : k * x = j * A.max' hne := by
        calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
          _ = j * ((A.max' hne).gcd x * k) := by ring
          _ = j * A.max' hne := by rw [← hk]
      have hkpos : 0 < k := by omega
      obtain ⟨hdvd, hmem⟩ := hS k (Finset.mem_range.2 hkn) j (Finset.mem_range.2 hjk) hj1
      obtain ⟨q, hq⟩ := hdvd
      refine ⟨L * j / k, hmem, ?_⟩
      rw [hq, Nat.mul_div_cancel_left q hkpos]
      apply Nat.eq_of_mul_eq_mul_left hkpos
      calc k * (L * x) = L * (k * x) := by ring
        _ = L * (j * A.max' hne) := by rw [hkx]
        _ = (L * j) * A.max' hne := by ring
        _ = (k * q) * A.max' hne := by rw [hq]
        _ = k * (q * A.max' hne) := by ring
    have hmaps : ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - 2) := by
      intro x hx
      obtain ⟨a, ha, hax⟩ := forms x hx
      rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
      have := hc a ha
      omega
    have hcardE : (A.erase (A.max' hne)).card = n - 1 := by
      rw [Finset.card_erase_of_mem hM, hcard]
    obtain ⟨x, hx, y, hy, hxy, hcol⟩ :=
      Finset.exists_ne_map_eq_of_card_lt_of_maps_to
        (by rw [hcardE, Finset.card_range]; omega) hmaps
    obtain ⟨a, ha, hax⟩ := forms x hx
    obtain ⟨b, hb, hby⟩ := forms y hy
    rw [hax, hby, Nat.mul_div_cancel _ hMpos, Nat.mul_div_cancel _ hMpos] at hcol
    have hab : a ≠ b := by
      intro h
      apply hxy
      apply Nat.eq_of_mul_eq_mul_left hL
      rw [hax, hby, h]
    have hgcd : a.gcd b * A.max' hne = L * x.gcd y := by
      have h1 : Nat.gcd (L * x) (L * y) = L * x.gcd y := Nat.gcd_mul_left L x y
      rw [hax, hby, Nat.gcd_mul_right] at h1
      exact h1
    have hxA := (Finset.mem_erase.mp hx).2
    have hyA := (Finset.mem_erase.mp hy).2
    rcases hgood a ha b hb hab hcol with h | h
    · refine ⟨x, hxA, y, hyA, key x y ?_⟩
      rw [hcard]
      have h2 : L * (x.gcd y * n) ≤ L * x := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * x := hax.symm
      exact Nat.le_of_mul_le_mul_left h2 hL
    · refine ⟨y, hyA, x, hxA, key y x ?_⟩
      rw [hcard, Nat.gcd_comm]
      have h2 : L * (x.gcd y * n) ≤ L * y := by
        calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
          _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
          _ = L * y := hby.symm
      exact Nat.le_of_mul_le_mul_left h2 hL
  exact red 18 12252240 {720720, 765765, 816816, 875160, 942480, 1021020, 1113840, 1225224, 1361360, 1441440, 1531530, 1633632, 1750320, 1884960, 2042040, 2162160, 2227680, 2297295, 2450448, 2625480, 2722720, 2827440, 2882880, 3063060, 3267264, 3341520, 3500640, 3603600, 3675672, 3769920, 3828825, 4084080, 4324320, 4375800, 4455360, 4594590, 4712400, 4900896, 5045040, 5105100, 5250960, 5360355, 5445440, 5569200, 5654880, 5717712, 5765760, 6126120, 6486480, 6534528, 6597360, 6683040, 6806800, 6891885, 7001280, 7147140, 7207200, 7351344, 7539840, 7657650, 7796880, 7876440, 7927920, 8168160, 8423415, 8482320, 8576568, 8648640, 8751600, 8910720, 8984976, 9189180, 9369360, 9424800, 9529520, 9626760, 9801792, 9954945, 10024560, 10090080, 10210200, 10367280, 10501920, 10618608, 10720710, 10810800, 10890880, 11027016, 11138400, 11231220, 11309760, 11377080, 11435424, 11486475, 11531520}
    (fun a : ℕ => if a = 720720 then 12 else if a = 765765 then 10 else if a = 816816 then 13 else if a = 875160 then 14 else if a = 942480 then 4 else if a = 1021020 then 7 else if a = 1113840 then 9 else if a = 1225224 then 3 else if a = 1361360 then 15 else if a = 1441440 then 13 else if a = 1531530 then 8 else if a = 1633632 then 4 else if a = 1750320 then 11 else if a = 1884960 then 14 else if a = 2042040 then 5 else if a = 2162160 then 3 else if a = 2227680 then 12 else if a = 2297295 then 11 else if a = 2450448 then 6 else if a = 2625480 then 7 else if a = 2722720 then 9 else if a = 2827440 then 12 else if a = 2882880 then 11 else if a = 3063060 then 2 else if a = 3267264 then 8 else if a = 3341520 then 13 else if a = 3500640 then 10 else if a = 3603600 then 4 else if a = 3675672 then 10 else if a = 3769920 then 5 else if a = 3828825 then 3 else if a = 4084080 then 1 else if a = 4324320 then 2 else if a = 4375800 then 9 else if a = 4455360 then 14 else if a = 4594590 then 9 else if a = 4712400 then 7 else if a = 4900896 then 7 else if a = 5045040 then 7 else if a = 5105100 then 10 else if a = 5250960 then 8 else if a = 5360355 then 12 else if a = 5445440 then 6 else if a = 5569200 then 5 else if a = 5654880 then 10 else if a = 5717712 then 2 else if a = 5765760 then 5 else if a = 6126120 then 0 else if a = 6486480 then 6 else if a = 6534528 then 11 else if a = 6597360 then 6 else if a = 6683040 then 6 else if a = 6806800 then 11 else if a = 6891885 then 7 else if a = 7001280 then 4 else if a = 7147140 then 11 else if a = 7207200 then 1 else if a = 7351344 then 5 else if a = 7539840 then 1 else if a = 7657650 then 6 else if a = 7796880 then 3 else if a = 7876440 then 3 else if a = 7927920 then 0 else if a = 8168160 then 3 else if a = 8423415 then 13 else if a = 8482320 then 8 else if a = 8576568 then 1 else if a = 8648640 then 8 else if a = 8751600 then 2 else if a = 8910720 then 2 else if a = 8984976 then 10 else if a = 9189180 then 4 else if a = 9369360 then 10 else if a = 9424800 then 0 else if a = 9529520 then 4 else if a = 9626760 then 6 else if a = 9801792 then 9 else if a = 9954945 then 1 else if a = 10024560 then 0 else if a = 10090080 then 14 else if a = 10210200 then 8 else if a = 10367280 then 2 else if a = 10501920 then 1 else if a = 10618608 then 12 else if a = 10720710 then 5 else if a = 10810800 then 9 else if a = 10890880 then 7 else if a = 11027016 then 2 else if a = 11138400 then 4 else if a = 11231220 then 9 else if a = 11309760 then 3 else if a = 11377080 then 5 else if a = 11435424 then 0 else if a = 11486475 then 14 else if a = 11531520 then 15 else 0)
    (by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel) (by decide +kernel) A hA hn

What is known

Work on it

No explainer yet. This proof written as a journal would print it, labelled unverified, is the next thing a writer could add, by pull request (D-3, D-36; the guide shows how).

Write the explainer →

How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →

Record

Statement: the Lean file and its words (1 version)

Statement not audited — only a problem’s root statement is audited for fidelity (D-9); the kernel checks a proof against this Lean as written.

import Mathlib
import Nodes.«variant-b89de5c4».Context

/-! Graham's gcd conjecture (Erdős problem 402) for eighteen-element sets. With M the largest
element, if gcd(M, x) > M/18 for every x then every other x is (j/k)M with j < k ≤ 17, so
L·x/M (L = lcm(1..17) = 12252240) lies in a fixed set S of 95 values. S splits into 16 classes in
each of which any two distinct values c, d have 18·gcd(c, d) ≤ c or ≤ d; by pigeonhole two of
the 17 other elements share a class, and gcd(x, y)·L = gcd(c, d)·M transfers the bound. -/

theorem Opn.erdos_402_card_eighteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 18 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  sorry

A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 18 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

Every set A of exactly eighteen positive integers has a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

Rendered from gloss/3bca86bd5924….md · Improve these words →

Rendered from targets/erdos-402/nodes/variant-b89de5c4/Statement.lean. Origin: variant (partial).

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000279.json, merge commit 423883f8a194.

Verdict pass, from attestations/000279.json.

Submitter
t0929-6
Toolchain
leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib
0df444a360eaa60ab8c11dca51a86af692955474
Reviewer
none needed (calibration)
StepCheckResult
1toolchainpass
2pathspass
4kernel-replaypass
5axiomspass
6hazardspass
7witnesspass
8depspass
Witness

Checked by the kernel — step 7 passed in the run its attestation records: attestations/000279.json, merge commit 423883f8a194.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/variant-b89de5c4/Witness.lean, sha256 45dd897aff78.
import Mathlib

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 18 :=
  ⟨Finset.Icc 1 18, by simp, by simp⟩

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Relation to the problem’s statement

Checked by the kernel — checked at admission (D-30); no proof of the node is implied.

Relation.lean — the implication between this variant and the problem’s statement, checked by the gate when the variant was admitted and immutable after (D-30). Rendered from targets/erdos-402/nodes/variant-b89de5c4/Relation.lean, sha256 d4da5e5f9ee5.
-- relation: partial
import Mathlib

theorem relation :
    (∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ᵉ (a ∈ A) (b ∈ A), a.gcd b ≤ (a / A.card : ℚ)) →
    (∀ (A : Finset ℕ), 0 ∉ A → A.card = 18 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) :=
  fun h A hA hn => h A hA (Finset.card_pos.mp (by omega))

No gloss yet: no one has written in words what this relation says (D-3 v3.30); the Lean above is the relation. How to write one →

Acknowledged findings (1)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at ↑a / ↑A.card

The hypothesis A.card = 18 makes A.card positive, so the rational division is never by zero.

How to read this page

How to read a statement’s page →