Open Proof Network

Problems / erdos-402 / variant-a874fe93

A prime element at least |A|

variant-a874fe93

proved

A partial route to the problem.

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

For a finite set A of positive integers containing a prime p with |A| ≤ p, there are a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

unverified · history

Lean
theorem Opn.erdos_402_large_prime :
    ∀ (A : Finset ℕ), 0 ∉ A → ∀ p ∈ A, p.Prime → A.card ≤ p →
      ∃ 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, 000182, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000182.json, merge commit d224f7df47c0.

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. hn have A.card ≤ x.minFac

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

    Lean, line 13
      have hn : A.card ≤ x.minFac := by rw [hxp.minFac_eq]; exact hn0

    targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 13 at d224f7df47c0 ↗

  2. hxpos have (0 : ℕ) < x

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

    Uses library Nat.pos_of_ne_zero.

    Lean, line 14
      have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA0 (h ▸ hx))

    targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 14 at d224f7df47c0 ↗

  3. hcard have (0 : ℕ) < A.card

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

    Uses library Finset.card_pos, Exists.intro Existential introduction. .

    Lean, line 15
      have hcard : 0 < A.card := Finset.card_pos.mpr ⟨x, hx⟩

    targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 15 at d224f7df47c0 ↗

  4. hcardQ have (0 : ℚ) < (↑A.card : ℚ)

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

    Lean, line 16
      have hcardQ : (0:ℚ) < A.card := by exact_mod_cast hcard

    targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 16 at d224f7df47c0 ↗

  5. s5 case

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

    Uses library Exists.intro Existential introduction. , le_div_iff₀ See le_div_iff₀' for a version with multiplication on the other side. .

    Lean, lines 18–39
      · obtain ⟨b, hb, hxb⟩ := h
    refine ⟨x, hx, b, hb, ?_⟩
    have hgpos : 0 < x.gcd b := Nat.gcd_pos_of_pos_left b hxpos
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left x b
    have hk1 : k ≠ 1 := by
      rintro rfl
      apply hxb
      have h2 : x = x.gcd b := by rw [mul_one] at hk; exact hk
      rw [h2]
      exact Nat.gcd_dvd_right x b
    have hkpos : 0 < k := by
      rcases Nat.eq_zero_or_pos k with h0 | h0
      · rw [h0, mul_zero] at hk; omega
      · exact h0
    have hkdvd : k ∣ x := ⟨x.gcd b, by rw [mul_comm]; exact hk⟩
    have hmin : x.minFac ≤ k := Nat.minFac_le_of_dvd (by omega) hkdvd
    have hnk : A.card ≤ k := le_trans hn hmin
    rw [le_div_iff₀ hcardQ]
    have key : x.gcd b * A.card ≤ x := by
      calc x.gcd b * A.card ≤ x.gcd b * k := Nat.mul_le_mul_left _ hnk
        _ = x := hk.symm
    exact_mod_cast key

    targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 18–39 at d224f7df47c0 ↗

    1. s5.s1 obtain ∃ b ∈ A, ¬x ∣ b

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with b : ℕ, hb : b ∈ A, hxb : ¬x ∣ b.

      Lean, line 18
        · obtain ⟨b, hb, hxb⟩ := h

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 18 at d224f7df47c0 ↗

    2. s5.hgpos have (0 : ℕ) < x.gcd b

      Leaves (↑(x.gcd b) : ℚ) ≤ (↑x : ℚ) / (↑A.card : ℚ), with hgpos : (0 : ℕ) < x.gcd b.

      Uses library Nat.gcd_pos_of_pos_left.

      Lean, line 20
          have hgpos : 0 < x.gcd b := Nat.gcd_pos_of_pos_left b hxpos

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 20 at d224f7df47c0 ↗

    3. s5.s3 obtain x.gcd b ∣ x

      Leaves (↑(x.gcd b) : ℚ) ≤ (↑x : ℚ) / (↑A.card : ℚ), with k : ℕ, hk : x = x.gcd b * k.

      Uses library Nat.gcd_dvd_left.

      Lean, line 21
          obtain ⟨k, hk⟩ := Nat.gcd_dvd_left x b

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 21 at d224f7df47c0 ↗

    4. s5.hk1 have k ≠ (1 : ℕ)

      Leaves (↑(x.gcd b) : ℚ) ≤ (↑x : ℚ) / (↑A.card : ℚ), with hk1 : k ≠ (1 : ℕ).

      Uses library Nat.gcd_dvd_right.

      Lean, lines 22–27
          have hk1 : k ≠ 1 := by
      rintro rfl
      apply hxb
      have h2 : x = x.gcd b := by rw [mul_one] at hk; exact hk
      rw [h2]
      exact Nat.gcd_dvd_right x b

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 22–27 at d224f7df47c0 ↗

      1. s5.hk1.h2 have x = x.gcd b

        Leaves x ∣ b, with h2 : x = x.gcd b.

        Uses library mul_one.

        Lean, line 25
              have h2 : x = x.gcd b := by rw [mul_one] at hk; exact hk

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 25 at d224f7df47c0 ↗

    5. s5.hkpos have (0 : ℕ) < k

      Leaves (↑(x.gcd b) : ℚ) ≤ (↑x : ℚ) / (↑A.card : ℚ), with hkpos : (0 : ℕ) < k.

      Uses library Nat.eq_zero_or_pos.

      Lean, lines 28–31
          have hkpos : 0 < k := by
      rcases Nat.eq_zero_or_pos k with h0 | h0
      · rw [h0, mul_zero] at hk; omega
      · exact h0

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 28–31 at d224f7df47c0 ↗

      1. s5.hkpos.s1 case

        Leaves (0 : ℕ) < k.

        Uses library MulZeroClass.mul_zero Zero is a right absorbing element for multiplication .

        Lean, line 30
              · rw [h0, mul_zero] at hk; omega

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 30 at d224f7df47c0 ↗

      2. s5.hkpos.s2 case

        Leaves (0 : ℕ) < k.

        Lean, line 31
              · exact h0

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 31 at d224f7df47c0 ↗

    6. s5.hkdvd have k ∣ x

      Leaves (↑(x.gcd b) : ℚ) ≤ (↑x : ℚ) / (↑A.card : ℚ), with hkdvd : k ∣ x.

      Uses library Exists.intro Existential introduction. , mul_comm.

      Lean, line 32
          have hkdvd : k ∣ x := ⟨x.gcd b, by rw [mul_comm]; exact hk⟩

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 32 at d224f7df47c0 ↗

    7. s5.hmin have x.minFac ≤ k

      Leaves (↑(x.gcd b) : ℚ) ≤ (↑x : ℚ) / (↑A.card : ℚ), with hmin : x.minFac ≤ k.

      Uses library Nat.minFac_le_of_dvd.

      Lean, line 33
          have hmin : x.minFac ≤ k := Nat.minFac_le_of_dvd (by omega) hkdvd

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 33 at d224f7df47c0 ↗

    8. s5.hnk have A.card ≤ k

      Leaves (↑(x.gcd b) : ℚ) ≤ (↑x : ℚ) / (↑A.card : ℚ), with hnk : A.card ≤ k.

      Uses library le_trans The relation ≤ on a preorder is transitive. .

      Lean, line 34
          have hnk : A.card ≤ k := le_trans hn hmin

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 34 at d224f7df47c0 ↗

    9. s5.key have x.gcd b * A.card ≤ x

      Leaves (↑(x.gcd b) : ℚ) * (↑A.card : ℚ) ≤ (↑x : ℚ), with key : x.gcd b * A.card ≤ x.

      Lean, lines 36–38
          have key : x.gcd b * A.card ≤ x := by
      calc x.gcd b * A.card ≤ x.gcd b * k := Nat.mul_le_mul_left _ hnk
        _ = x := hk.symm

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 36–38 at d224f7df47c0 ↗

      1. s5.key.s1 calc x.gcd b * A.card ≤ x.gcd b * k

        Closes the goal.

        Uses library Nat.mul_le_mul_left.

        Lean, line 37
              calc x.gcd b * A.card ≤ x.gcd b * k := Nat.mul_le_mul_left _ hnk

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 37 at d224f7df47c0 ↗

      2. s5.key.s2 calc x.gcd b * k = x

        Closes the goal.

        Lean, line 38
                _ = x := hk.symm

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 38 at d224f7df47c0 ↗

  6. s6 case

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

    Uses library Not Not p, or ¬p, is the negation of p. , Exists.intro Existential introduction. , le_div_iff₀ See le_div_iff₀' for a version with multiplication on the other side. .

    Lean, lines 40–67
      · push Not at h
    have hne : A.Nonempty := ⟨x, hx⟩
    have hMA : A.max' hne ∈ A := Finset.max'_mem A hne
    have hxM : x ∣ A.max' hne := h _ hMA
    refine ⟨A.max' hne, hMA, x, hx, ?_⟩
    have hgcd : (A.max' hne).gcd x = x := Nat.gcd_eq_right hxM
    rw [hgcd, le_div_iff₀ hcardQ]
    have hsub : A ⊆ (Finset.Icc 1 (A.max' hne / x)).image (fun i => x * i) := by
      intro b hb
      obtain ⟨i, rfl⟩ := h b hb
      rw [Finset.mem_image]
      refine ⟨i, ?_, rfl⟩
      rw [Finset.mem_Icc]
      constructor
      · rcases Nat.eq_zero_or_pos i with h0 | h0
        · exfalso; apply hA0; rw [h0, mul_zero] at hb; exact hb
        · exact h0
      · rw [Nat.le_div_iff_mul_le hxpos, mul_comm]
        exact Finset.le_max' A _ hb
    have hc : A.card ≤ A.max' hne / x := by
      calc A.card ≤ ((Finset.Icc 1 (A.max' hne / x)).image (fun i => x * i)).card :=
            Finset.card_le_card hsub
        _ ≤ (Finset.Icc 1 (A.max' hne / x)).card := Finset.card_image_le
        _ = A.max' hne / x := by simp
    have key : x * A.card ≤ A.max' hne := by
      calc x * A.card ≤ x * (A.max' hne / x) := Nat.mul_le_mul_left x hc
        _ ≤ A.max' hne := Nat.mul_div_le _ x
    exact_mod_cast key

    targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 40–67 at d224f7df47c0 ↗

    1. s6.hne have A.Nonempty

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

      Uses library Exists.intro Existential introduction. .

      Lean, line 41
          have hne : A.Nonempty := ⟨x, hx⟩

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 41 at d224f7df47c0 ↗

    2. s6.hMA have A.max' hne ∈ A

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

      Uses library Finset.max'_mem.

      Lean, line 42
          have hMA : A.max' hne ∈ A := Finset.max'_mem A hne

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 42 at d224f7df47c0 ↗

    3. s6.hxM have x ∣ A.max' hne

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

      Lean, line 43
          have hxM : x ∣ A.max' hne := h _ hMA

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 43 at d224f7df47c0 ↗

    4. s6.hgcd have (A.max' hne).gcd x = x

      Leaves (↑((A.max' hne).gcd x) : ℚ) ≤ (↑(A.max' hne) : ℚ) / (↑A.card : ℚ), with hgcd : (A.max' hne).gcd x = x.

      Uses library Nat.gcd_eq_right.

      Lean, line 45
          have hgcd : (A.max' hne).gcd x = x := Nat.gcd_eq_right hxM

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 45 at d224f7df47c0 ↗

    5. s6.hsub have A ⊆ Finset.image (fun (i : ℕ) => x * i) (Finset.Icc (1 : ℕ) (A.max' hne / x))

      Leaves (↑x : ℚ) * (↑A.card : ℚ) ≤ (↑(A.max' hne) : ℚ), with hsub : A ⊆ Finset.image (fun (i : ℕ) => x * i) (Finset.Icc (1 : ℕ) (A.max' hne / x)).

      Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Finset.mem_image, Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. , Finset.mem_Icc.

      Lean, lines 47–58
          have hsub : A ⊆ (Finset.Icc 1 (A.max' hne / x)).image (fun i => x * i) := by
      intro b hb
      obtain ⟨i, rfl⟩ := h b hb
      rw [Finset.mem_image]
      refine ⟨i, ?_, rfl⟩
      rw [Finset.mem_Icc]
      constructor
      · rcases Nat.eq_zero_or_pos i with h0 | h0
        · exfalso; apply hA0; rw [h0, mul_zero] at hb; exact hb
        · exact h0
      · rw [Nat.le_div_iff_mul_le hxpos, mul_comm]
        exact Finset.le_max' A _ hb

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 47–58 at d224f7df47c0 ↗

      1. s6.hsub.s1 obtain x ∣ b

        Leaves x * i ∈ Finset.image (fun (i : ℕ) => x * i) (Finset.Icc (1 : ℕ) (A.max' hne / x)), with i : ℕ, hb : x * i ∈ A.

        Lean, line 49
              obtain ⟨i, rfl⟩ := h b hb

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 49 at d224f7df47c0 ↗

      2. s6.hsub.s2 case

        Leaves (1 : ℕ) ≤ i.

        Uses library Nat.eq_zero_or_pos.

        Lean, lines 54–56
              · rcases Nat.eq_zero_or_pos i with h0 | h0
        · exfalso; apply hA0; rw [h0, mul_zero] at hb; exact hb
        · exact h0

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 54–56 at d224f7df47c0 ↗

        1. s6.hsub.s2.s1 case

          Leaves (1 : ℕ) ≤ i.

          Uses library MulZeroClass.mul_zero Zero is a right absorbing element for multiplication .

          Lean, line 55
                  · exfalso; apply hA0; rw [h0, mul_zero] at hb; exact hb

          targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 55 at d224f7df47c0 ↗

        2. s6.hsub.s2.s2 case

          Leaves (1 : ℕ) ≤ i.

          Lean, line 56
                  · exact h0

          targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 56 at d224f7df47c0 ↗

      3. s6.hsub.s3 case

        Leaves i ≤ A.max' hne / x.

        Uses library Nat.le_div_iff_mul_le, mul_comm, Finset.le_max'.

        Lean, lines 57–58
              · rw [Nat.le_div_iff_mul_le hxpos, mul_comm]
        exact Finset.le_max' A _ hb

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 57–58 at d224f7df47c0 ↗

    6. s6.hc have A.card ≤ A.max' hne / x

      Leaves (↑x : ℚ) * (↑A.card : ℚ) ≤ (↑(A.max' hne) : ℚ), with hc : A.card ≤ A.max' hne / x.

      Lean, lines 59–63
          have hc : A.card ≤ A.max' hne / x := by
      calc A.card ≤ ((Finset.Icc 1 (A.max' hne / x)).image (fun i => x * i)).card :=
            Finset.card_le_card hsub
        _ ≤ (Finset.Icc 1 (A.max' hne / x)).card := Finset.card_image_le
        _ = A.max' hne / x := by simp

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 59–63 at d224f7df47c0 ↗

      1. s6.hc.s1 calc A.card ≤ (Finset.image (fun (i : ℕ) => x * i) (Finset.Icc (1 : ℕ) (A.max' hne / x))).card

        Closes the goal.

        Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Finset.card_le_card.

        Lean, lines 60–61
              calc A.card ≤ ((Finset.Icc 1 (A.max' hne / x)).image (fun i => x * i)).card :=
            Finset.card_le_card hsub

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 60–61 at d224f7df47c0 ↗

      2. s6.hc.s2 calc (Finset.image (fun (i : ℕ) => x * i) (Finset.Icc (1 : ℕ) (A.max' hne / x))).card ≤ (Finset.Icc (1 : ℕ) (A.max' hne / x)).card

        Closes the goal.

        Uses library Finset.Icc The finset $[a, b]$ of elements x such that a ≤ x and x ≤ b. , Finset.card_image_le.

        Lean, line 62
                _ ≤ (Finset.Icc 1 (A.max' hne / x)).card := Finset.card_image_le

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 62 at d224f7df47c0 ↗

      3. s6.hc.s3 calc routine: simp

        Closes the goal.

        Lean, line 63
                _ = A.max' hne / x := by simp

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 63 at d224f7df47c0 ↗

    7. s6.key have x * A.card ≤ A.max' hne

      Leaves (↑x : ℚ) * (↑A.card : ℚ) ≤ (↑(A.max' hne) : ℚ), with key : x * A.card ≤ A.max' hne.

      Lean, lines 64–66
          have key : x * A.card ≤ A.max' hne := by
      calc x * A.card ≤ x * (A.max' hne / x) := Nat.mul_le_mul_left x hc
        _ ≤ A.max' hne := Nat.mul_div_le _ x

      targets/erdos-402/nodes/variant-a874fe93/Proof.lean, lines 64–66 at d224f7df47c0 ↗

      1. s6.key.s1 calc x * A.card ≤ x * (A.max' hne / x)

        Closes the goal.

        Uses library Nat.mul_le_mul_left.

        Lean, line 65
              calc x * A.card ≤ x * (A.max' hne / x) := Nat.mul_le_mul_left x hc

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 65 at d224f7df47c0 ↗

      2. s6.key.s2 calc x * (A.max' hne / x) ≤ A.max' hne

        Closes the goal.

        Uses library Nat.mul_div_le.

        Lean, line 66
                _ ≤ A.max' hne := Nat.mul_div_le _ x

        targets/erdos-402/nodes/variant-a874fe93/Proof.lean, line 66 at d224f7df47c0 ↗

The proof in Lean (Proof.lean)

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

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

/-! Graham's gcd conjecture (Erdős problem 402) when `A` contains a prime `p ≥ |A|`. If some
`b ∈ A` is not a multiple of `p`, the pair `(p, b)` has gcd 1 and `1 ≤ p / |A|`. Otherwise every
element is a multiple of `p` at most `max A`, so `|A| ≤ max A / p`, and the pair `(max A, p)` has
gcd `p ≤ max A / |A|`. -/

theorem Opn.erdos_402_large_prime :
    ∀ (A : Finset ℕ), 0 ∉ A → ∀ p ∈ A, p.Prime → A.card ≤ p →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A hA0 x hx hxp hn0
  have hn : A.card ≤ x.minFac := by rw [hxp.minFac_eq]; exact hn0
  have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA0 (h ▸ hx))
  have hcard : 0 < A.card := Finset.card_pos.mpr ⟨x, hx⟩
  have hcardQ : (0:ℚ) < A.card := by exact_mod_cast hcard
  by_cases h : ∃ b ∈ A, ¬ x ∣ b
  · obtain ⟨b, hb, hxb⟩ := h
    refine ⟨x, hx, b, hb, ?_⟩
    have hgpos : 0 < x.gcd b := Nat.gcd_pos_of_pos_left b hxpos
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left x b
    have hk1 : k ≠ 1 := by
      rintro rfl
      apply hxb
      have h2 : x = x.gcd b := by rw [mul_one] at hk; exact hk
      rw [h2]
      exact Nat.gcd_dvd_right x b
    have hkpos : 0 < k := by
      rcases Nat.eq_zero_or_pos k with h0 | h0
      · rw [h0, mul_zero] at hk; omega
      · exact h0
    have hkdvd : k ∣ x := ⟨x.gcd b, by rw [mul_comm]; exact hk⟩
    have hmin : x.minFac ≤ k := Nat.minFac_le_of_dvd (by omega) hkdvd
    have hnk : A.card ≤ k := le_trans hn hmin
    rw [le_div_iff₀ hcardQ]
    have key : x.gcd b * A.card ≤ x := by
      calc x.gcd b * A.card ≤ x.gcd b * k := Nat.mul_le_mul_left _ hnk
        _ = x := hk.symm
    exact_mod_cast key
  · push Not at h
    have hne : A.Nonempty := ⟨x, hx⟩
    have hMA : A.max' hne ∈ A := Finset.max'_mem A hne
    have hxM : x ∣ A.max' hne := h _ hMA
    refine ⟨A.max' hne, hMA, x, hx, ?_⟩
    have hgcd : (A.max' hne).gcd x = x := Nat.gcd_eq_right hxM
    rw [hgcd, le_div_iff₀ hcardQ]
    have hsub : A ⊆ (Finset.Icc 1 (A.max' hne / x)).image (fun i => x * i) := by
      intro b hb
      obtain ⟨i, rfl⟩ := h b hb
      rw [Finset.mem_image]
      refine ⟨i, ?_, rfl⟩
      rw [Finset.mem_Icc]
      constructor
      · rcases Nat.eq_zero_or_pos i with h0 | h0
        · exfalso; apply hA0; rw [h0, mul_zero] at hb; exact hb
        · exact h0
      · rw [Nat.le_div_iff_mul_le hxpos, mul_comm]
        exact Finset.le_max' A _ hb
    have hc : A.card ≤ A.max' hne / x := by
      calc A.card ≤ ((Finset.Icc 1 (A.max' hne / x)).image (fun i => x * i)).card :=
            Finset.card_le_card hsub
        _ ≤ (Finset.Icc 1 (A.max' hne / x)).card := Finset.card_image_le
        _ = A.max' hne / x := by simp
    have key : x * A.card ≤ A.max' hne := by
      calc x * A.card ≤ x * (A.max' hne / x) := Nat.mul_le_mul_left x hc
        _ ≤ A.max' hne := Nat.mul_div_le _ x
    exact_mod_cast key
Alternate proofs (1)

Later proofs of the same statement, kept beside the first because a different proof can carry a different insight (D-25). Each passed the gate as a proof does; none changes this node's status or credit.

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-a874fe93».Context

/-! Graham's gcd conjecture (Erdős problem 402) when `A` contains a prime `p ≥ |A|`. If some
`b ∈ A` is not a multiple of `p`, the pair `(p, b)` has gcd 1 and `1 ≤ p / |A|`. Otherwise every
element is a multiple of `p` at most `max A`, so `|A| ≤ max A / p`, and the pair `(max A, p)` has
gcd `p ≤ max A / |A|`. -/

theorem Opn.erdos_402_large_prime :
    ∀ (A : Finset ℕ), 0 ∉ A → ∀ p ∈ A, p.Prime → A.card ≤ p →
      ∃ 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 \Rightarrow \forall p \in A,\ p\ \text{prime},\ |A| \le p \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

For a finite set A of positive integers containing a prime p with |A| ≤ p, there are a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

Rendered from gloss/8078657976ff….md · Improve these words →

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000182.json, merge commit d224f7df47c0.

Verdict pass, from attestations/000182.json.

Submitter
tester-402-mcp
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/000182.json, merge commit d224f7df47c0.

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

theorem witness : ∃ (A : Finset ℕ) (p : ℕ), 0 ∉ A ∧ p ∈ A ∧ p.Prime ∧ A.card ≤ p :=
  ⟨{2}, 2, by decide, by simp, Nat.prime_two, 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-a874fe93/Relation.lean, sha256 a1beeb4e2992.
-- 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 → ∀ p ∈ A, p.Prime → A.card ≤ p →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) := by
  intro h A hA p hp _ _
  obtain ⟨a, ha, b, hb, hab⟩ := h A hA ⟨p, hp⟩
  exact ⟨a, ha, b, hb, hab⟩

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 gives p ∈ A, so A is nonempty and A.card > 0; the rational division is never by zero.

How to read this page

How to read a statement’s page →