Open Proof Network

Problems / erdos-402 / variant-64035064

Graham's bound for |A| = 16

variant-64035064

proved

A partial route to the problem.

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

Every set A of exactly sixteen 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_sixteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 16 → ∃ 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, 000264, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000264.json, merge commit 068a43e8f246.

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-64035064/Proof.lean, lines 13–111 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 20 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 21 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 22–25 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 26 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 27 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 29–30 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 29 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 32–71 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 35 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 36 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 37 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 38 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 39 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 40 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 41 at 068a43e8f246 ↗

      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-64035064/Proof.lean, lines 42–46 at 068a43e8f246 ↗

        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-64035064/Proof.lean, lines 44–45 at 068a43e8f246 ↗

        2. red.forms.hj1.s2 case

          Leaves (0 : ℕ) < j.

          Lean, line 46
                  · exact h

          targets/erdos-402/nodes/variant-64035064/Proof.lean, line 46 at 068a43e8f246 ↗

      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-64035064/Proof.lean, lines 47–51 at 068a43e8f246 ↗

        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-64035064/Proof.lean, lines 48–50 at 068a43e8f246 ↗

      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-64035064/Proof.lean, lines 52–56 at 068a43e8f246 ↗

        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-64035064/Proof.lean, lines 53–55 at 068a43e8f246 ↗

      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-64035064/Proof.lean, lines 57–60 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 58 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 59 at 068a43e8f246 ↗

        3. red.forms.hkx.s3 calc

          Closes the goal.

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

          targets/erdos-402/nodes/variant-64035064/Proof.lean, line 60 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 61 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 62 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 63 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 67 at 068a43e8f246 ↗

      16. red.forms.s16 calc

        Closes the goal.

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

        targets/erdos-402/nodes/variant-64035064/Proof.lean, line 68 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 69 at 068a43e8f246 ↗

      18. red.forms.s18 calc

        Closes the goal.

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

        targets/erdos-402/nodes/variant-64035064/Proof.lean, line 70 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 71 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 72–77 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 74 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 76 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 78–79 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 80–82 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 83 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 84 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 86–90 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 91–94 at 068a43e8f246 ↗

      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-64035064/Proof.lean, line 92 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 95 at 068a43e8f246 ↗

    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-64035064/Proof.lean, line 96 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 98–104 at 068a43e8f246 ↗

      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-64035064/Proof.lean, lines 100–103 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 101 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 102 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 103 at 068a43e8f246 ↗

    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-64035064/Proof.lean, lines 105–111 at 068a43e8f246 ↗

      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-64035064/Proof.lean, lines 107–110 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 108 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 109 at 068a43e8f246 ↗

        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-64035064/Proof.lean, line 110 at 068a43e8f246 ↗

The proof in Lean (Proof.lean)

Checked by the kernel — these bytes are the ones its attestation names: attestations/000264.json, merge commit 068a43e8f246.

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-64035064/Proof.lean, sha256 4684fe4a7920.
import Mathlib
import Nodes.«variant-64035064».Context

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

theorem Opn.erdos_402_card_sixteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 16 → ∃ 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 16 360360 {24024, 25740, 27720, 30030, 32760, 36036, 40040, 45045, 48048, 51480, 55440, 60060, 65520, 72072, 77220, 80080, 83160, 90090, 96096, 98280, 102960, 108108, 110880, 120120, 128700, 131040, 135135, 138600, 144144, 150150, 154440, 160160, 163800, 166320, 168168, 180180, 192192, 194040, 196560, 200200, 205920, 210210, 216216, 221760, 225225, 229320, 231660, 240240, 249480, 252252, 257400, 262080, 264264, 270270, 277200, 280280, 283140, 288288, 294840, 300300, 304920, 308880, 312312, 315315, 320320, 324324, 327600, 330330, 332640, 334620, 336336}
    (fun a : ℕ => if a = 24024 then 9 else if a = 25740 then 10 else if a = 27720 then 12 else if a = 30030 then 11 else if a = 32760 then 8 else if a = 36036 then 2 else if a = 40040 then 6 else if a = 45045 then 13 else if a = 48048 then 8 else if a = 51480 then 7 else if a = 55440 then 11 else if a = 60060 then 5 else if a = 65520 then 12 else if a = 72072 then 3 else if a = 77220 then 6 else if a = 80080 then 10 else if a = 83160 then 2 else if a = 90090 then 4 else if a = 96096 then 11 else if a = 98280 then 11 else if a = 102960 then 9 else if a = 108108 then 10 else if a = 110880 then 8 else if a = 120120 then 1 else if a = 128700 then 11 else if a = 131040 then 5 else if a = 135135 then 9 else if a = 138600 then 5 else if a = 144144 then 6 else if a = 150150 then 3 else if a = 154440 then 8 else if a = 160160 then 4 else if a = 163800 then 6 else if a = 166320 then 3 else if a = 168168 then 4 else if a = 180180 then 0 else if a = 192192 then 0 else if a = 194040 then 1 else if a = 196560 then 4 else if a = 200200 then 7 else if a = 205920 then 3 else if a = 210210 then 6 else if a = 216216 then 5 else if a = 221760 then 4 else if a = 225225 then 2 else if a = 229320 then 2 else if a = 231660 then 2 else if a = 240240 then 2 else if a = 249480 then 6 else if a = 252252 then 8 else if a = 257400 then 4 else if a = 262080 then 1 else if a = 264264 then 13 else if a = 270270 then 7 else if a = 277200 then 7 else if a = 280280 then 3 else if a = 283140 then 5 else if a = 288288 then 7 else if a = 294840 then 0 else if a = 300300 then 8 else if a = 304920 then 0 else if a = 308880 then 1 else if a = 312312 then 10 else if a = 315315 then 5 else if a = 320320 then 5 else if a = 324324 then 1 else if a = 327600 then 3 else if a = 330330 then 9 else if a = 332640 then 9 else if a = 334620 then 12 else if a = 336336 then 12 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-64035064».Context

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

theorem Opn.erdos_402_card_sixteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 16 → ∃ 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| = 16 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

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

Rendered from gloss/2adf3b3f64ea….md · Improve these words →

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000264.json, merge commit 068a43e8f246.

Verdict pass, from attestations/000264.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/000264.json, merge commit 068a43e8f246.

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

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 16 :=
  ⟨Finset.Icc 1 16, 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-64035064/Relation.lean, sha256 a266e0d97805.
-- 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 = 16 → ∃ 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 = 16 makes A.card positive, so the rational division is never by zero.

How to read this page

How to read a statement’s page →