Open Proof Network

Problems / erdos-402 / variant-3377fd96

An element whose least prime factor is at least |A|

variant-3377fd96

proved

A partial route to the problem.

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

For a finite set A of positive integers and any x ∈ A whose least prime factor is at least |A|, there are a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. minFac(x) is the least prime factor of x (minFac(1) = 1); the division is in ℚ.

unverified · history

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000177.json, merge commit 1ec050140378.

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. hpos have (0 : ℕ) < A.card

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

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

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

    targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 13 at 1ec050140378 ↗

  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 => hA (h ▸ hx))

    targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 14 at 1ec050140378 ↗

  3. 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 15–18
      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-3377fd96/Proof.lean, lines 15–18 at 1ec050140378 ↗

  4. s4 case

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

    Uses library Exists.intro Existential introduction. .

    Lean, lines 20–33
      · obtain ⟨b, hb, hlt⟩ := hc
    refine ⟨x, hx, b, hb, key x b ?_⟩
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left x b
    have hk2 : 2 ≤ k := by
      by_contra hcon
      push_neg at hcon
      interval_cases k
      · rw [mul_zero] at hk
        omega
      · rw [mul_one] at hk
        omega
    have hmk : x.minFac ≤ k := Nat.minFac_le_of_dvd hk2 ⟨x.gcd b, by rw [mul_comm]; exact hk⟩
    calc x.gcd b * A.card ≤ x.gcd b * k := Nat.mul_le_mul_left _ (hmin.trans hmk)
      _ = x := hk.symm

    targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 20–33 at 1ec050140378 ↗

    1. s4.s1 obtain ∃ b ∈ A, x.gcd b < x

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

      Lean, line 20
        · obtain ⟨b, hb, hlt⟩ := hc

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 20 at 1ec050140378 ↗

    2. s4.s2 obtain x.gcd b ∣ x

      Leaves x.gcd b * A.card ≤ x, with k : ℕ, hk : x = x.gcd b * k.

      Uses library Nat.gcd_dvd_left.

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

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 22 at 1ec050140378 ↗

    3. s4.hk2 have (2 : ℕ) ≤ k

      Leaves x.gcd b * A.card ≤ x, with hk2 : (2 : ℕ) ≤ k.

      Lean, lines 23–30
          have hk2 : 2 ≤ k := by
      by_contra hcon
      push_neg at hcon
      interval_cases k
      · rw [mul_zero] at hk
        omega
      · rw [mul_one] at hk
        omega

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 23–30 at 1ec050140378 ↗

      1. s4.hk2.s1 case

        Leaves False.

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

        Lean, lines 27–28
              · rw [mul_zero] at hk
        omega

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 27–28 at 1ec050140378 ↗

      2. s4.hk2.s2 case

        Leaves False.

        Uses library mul_one.

        Lean, lines 29–30
              · rw [mul_one] at hk
        omega

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 29–30 at 1ec050140378 ↗

    4. s4.hmk have x.minFac ≤ k

      Leaves x.gcd b * A.card ≤ x, with hmk : x.minFac ≤ k.

      Uses library Nat.minFac_le_of_dvd, Exists.intro Existential introduction. , mul_comm.

      Lean, line 31
          have hmk : x.minFac ≤ k := Nat.minFac_le_of_dvd hk2 ⟨x.gcd b, by rw [mul_comm]; exact hk⟩

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 31 at 1ec050140378 ↗

    5. s4.s5 calc x.gcd b * A.card ≤ x.gcd b * k

      Closes the goal.

      Uses library Nat.mul_le_mul_left.

      Lean, line 32
          calc x.gcd b * A.card ≤ x.gcd b * k := Nat.mul_le_mul_left _ (hmin.trans hmk)

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 32 at 1ec050140378 ↗

    6. s4.s6 calc x.gcd b * k = x

      Closes the goal.

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

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 33 at 1ec050140378 ↗

  5. s5 case

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

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

    Lean, lines 34–59
      · push_neg at hc
    have hdvd : ∀ b ∈ A, x ∣ b := fun b hb => by
      have h3 : x.gcd b = x := le_antisymm (Nat.gcd_le_left b hxpos) (hc b hb)
      rw [← h3]
      exact Nat.gcd_dvd_right x b
    have hMA : A.max' ⟨x, hx⟩ ∈ A := Finset.max'_mem A _
    refine ⟨A.max' ⟨x, hx⟩, hMA, x, hx, key _ x ?_⟩
    rw [Nat.gcd_eq_right (hdvd _ hMA)]
    have hsub : A ⊆ (Finset.Icc 1 (A.max' ⟨x, hx⟩ / x)).image (fun k => x * k) := by
      intro b hb
      obtain ⟨k, rfl⟩ := hdvd b hb
      rw [Finset.mem_image]
      refine ⟨k, Finset.mem_Icc.mpr ⟨?_, ?_⟩, rfl⟩
      · rcases Nat.eq_zero_or_pos k with h | h
        · subst h
          rw [mul_zero] at hb
          exact absurd hb hA
        · exact h
      · rw [Nat.le_div_iff_mul_le hxpos, mul_comm]
        exact Finset.le_max' A _ hb
    have hcard : A.card ≤ A.max' ⟨x, hx⟩ / x :=
      calc A.card ≤ _ := Finset.card_le_card hsub
        _ ≤ (Finset.Icc 1 (A.max' ⟨x, hx⟩ / x)).card := Finset.card_image_le
        _ = A.max' ⟨x, hx⟩ / x := by simp
    calc x * A.card ≤ x * (A.max' ⟨x, hx⟩ / x) := Nat.mul_le_mul_left x hcard
      _ ≤ A.max' ⟨x, hx⟩ := Nat.mul_div_le _ x

    targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 34–59 at 1ec050140378 ↗

    1. s5.hdvd have ∀ b ∈ A, x ∣ b

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

      Uses library Nat.gcd_dvd_right.

      Lean, lines 35–38
          have hdvd : ∀ b ∈ A, x ∣ b := fun b hb => by
      have h3 : x.gcd b = x := le_antisymm (Nat.gcd_le_left b hxpos) (hc b hb)
      rw [← h3]
      exact Nat.gcd_dvd_right x b

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 35–38 at 1ec050140378 ↗

      1. s5.hdvd.h3 have x.gcd b = x

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

        Uses library le_antisymm, Nat.gcd_le_left.

        Lean, line 36
              have h3 : x.gcd b = x := le_antisymm (Nat.gcd_le_left b hxpos) (hc b hb)

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 36 at 1ec050140378 ↗

    2. s5.hMA have A.max' ⋯ ∈ A

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

      Uses library Exists.intro Existential introduction. , Finset.max'_mem.

      Lean, line 39
          have hMA : A.max' ⟨x, hx⟩ ∈ A := Finset.max'_mem A _

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 39 at 1ec050140378 ↗

    3. s5.hsub have A ⊆ Finset.image (fun (k : ℕ) => x * k) (Finset.Icc (1 : ℕ) (A.max' ⋯ / x))

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

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

      Lean, lines 42–53
          have hsub : A ⊆ (Finset.Icc 1 (A.max' ⟨x, hx⟩ / x)).image (fun k => x * k) := by
      intro b hb
      obtain ⟨k, rfl⟩ := hdvd b hb
      rw [Finset.mem_image]
      refine ⟨k, Finset.mem_Icc.mpr ⟨?_, ?_⟩, rfl⟩
      · rcases Nat.eq_zero_or_pos k with h | h
        · subst h
          rw [mul_zero] at hb
          exact absurd hb hA
        · exact h
      · rw [Nat.le_div_iff_mul_le hxpos, mul_comm]
        exact Finset.le_max' A _ hb

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 42–53 at 1ec050140378 ↗

      1. s5.hsub.s1 obtain x ∣ b

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

        Lean, line 44
              obtain ⟨k, rfl⟩ := hdvd b hb

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 44 at 1ec050140378 ↗

      2. s5.hsub.s2 case

        Leaves (1 : ℕ) ≤ k.

        Uses library Nat.eq_zero_or_pos.

        Lean, lines 47–51
              · rcases Nat.eq_zero_or_pos k with h | h
        · subst h
          rw [mul_zero] at hb
          exact absurd hb hA
        · exact h

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 47–51 at 1ec050140378 ↗

        1. s5.hsub.s2.s1 case

          Leaves (1 : ℕ) ≤ k.

          Uses library MulZeroClass.mul_zero Zero is a right absorbing element for multiplication , absurd Anything follows from two contradictory hypotheses. .

          Lean, lines 48–50
                  · subst h
          rw [mul_zero] at hb
          exact absurd hb hA

          targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 48–50 at 1ec050140378 ↗

        2. s5.hsub.s2.s2 case

          Leaves (1 : ℕ) ≤ k.

          Lean, line 51
                  · exact h

          targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 51 at 1ec050140378 ↗

      3. s5.hsub.s3 case

        Leaves k ≤ A.max' ⋯ / x.

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

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

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 52–53 at 1ec050140378 ↗

    4. s5.hcard have A.card ≤ A.max' ⋯ / x

      Leaves x * A.card ≤ A.max' ⋯, with hcard : A.card ≤ A.max' ⋯ / x.

      Uses library Exists.intro Existential introduction. .

      Lean, lines 54–57
          have hcard : A.card ≤ A.max' ⟨x, hx⟩ / x :=
      calc A.card ≤ _ := Finset.card_le_card hsub
        _ ≤ (Finset.Icc 1 (A.max' ⟨x, hx⟩ / x)).card := Finset.card_image_le
        _ = A.max' ⟨x, hx⟩ / x := by simp

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, lines 54–57 at 1ec050140378 ↗

      1. s5.hcard.s1 calc A.card ≤ (Finset.image (fun (k : ℕ) => x * k) (Finset.Icc (1 : ℕ) (A.max' ⋯ / x))).card

        Closes the goal.

        Uses library Finset.card_le_card.

        Lean, line 55
              calc A.card ≤ _ := Finset.card_le_card hsub

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 55 at 1ec050140378 ↗

      2. s5.hcard.s2 calc (Finset.image (fun (k : ℕ) => x * k) (Finset.Icc (1 : ℕ) (A.max' ⋯ / x))).card ≤ (Finset.Icc (1 : ℕ) (A.max' ⋯ / x)).card

        Closes the goal.

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

        Lean, line 56
                _ ≤ (Finset.Icc 1 (A.max' ⟨x, hx⟩ / x)).card := Finset.card_image_le

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 56 at 1ec050140378 ↗

      3. s5.hcard.s3 calc routine: simp

        Closes the goal.

        Uses library Exists.intro Existential introduction. .

        Lean, line 57
                _ = A.max' ⟨x, hx⟩ / x := by simp

        targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 57 at 1ec050140378 ↗

    5. s5.s5 calc x * A.card ≤ x * (A.max' ⋯ / x)

      Closes the goal.

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

      Lean, line 58
          calc x * A.card ≤ x * (A.max' ⟨x, hx⟩ / x) := Nat.mul_le_mul_left x hcard

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 58 at 1ec050140378 ↗

    6. s5.s6 calc x * (A.max' ⋯ / x) ≤ A.max' ⋯

      Closes the goal.

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

      Lean, line 59
            _ ≤ A.max' ⟨x, hx⟩ := Nat.mul_div_le _ x

      targets/erdos-402/nodes/variant-3377fd96/Proof.lean, line 59 at 1ec050140378 ↗

The proof in Lean (Proof.lean)

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

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-3377fd96/Proof.lean, sha256 8a9004339085.
import Mathlib
import Nodes.«variant-3377fd96».Context

/-! Graham's gcd conjecture (Erdős problem 402) when some element `x` of `A` has no prime factor
below `|A|`: either `x` divides every element, and then the largest element is at least `|A| * x`,
or `gcd(x, b) < x` for some `b`, and then `x / gcd(x, b)` is a divisor of `x` above 1, so at
least `x.minFac ≥ |A|`. Contains the case of a prime `p ≥ |A|` in `A`. -/

theorem Opn.erdos_402_minFac :
    ∀ (A : Finset ℕ), 0 ∉ A → ∀ x ∈ A, A.card ≤ x.minFac →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A hA x hx hmin
  have hpos : 0 < A.card := Finset.card_pos.mpr ⟨x, hx⟩
  have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx))
  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
  by_cases hc : ∃ b ∈ A, x.gcd b < x
  · obtain ⟨b, hb, hlt⟩ := hc
    refine ⟨x, hx, b, hb, key x b ?_⟩
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left x b
    have hk2 : 2 ≤ k := by
      by_contra hcon
      push_neg at hcon
      interval_cases k
      · rw [mul_zero] at hk
        omega
      · rw [mul_one] at hk
        omega
    have hmk : x.minFac ≤ k := Nat.minFac_le_of_dvd hk2 ⟨x.gcd b, by rw [mul_comm]; exact hk⟩
    calc x.gcd b * A.card ≤ x.gcd b * k := Nat.mul_le_mul_left _ (hmin.trans hmk)
      _ = x := hk.symm
  · push_neg at hc
    have hdvd : ∀ b ∈ A, x ∣ b := fun b hb => by
      have h3 : x.gcd b = x := le_antisymm (Nat.gcd_le_left b hxpos) (hc b hb)
      rw [← h3]
      exact Nat.gcd_dvd_right x b
    have hMA : A.max' ⟨x, hx⟩ ∈ A := Finset.max'_mem A _
    refine ⟨A.max' ⟨x, hx⟩, hMA, x, hx, key _ x ?_⟩
    rw [Nat.gcd_eq_right (hdvd _ hMA)]
    have hsub : A ⊆ (Finset.Icc 1 (A.max' ⟨x, hx⟩ / x)).image (fun k => x * k) := by
      intro b hb
      obtain ⟨k, rfl⟩ := hdvd b hb
      rw [Finset.mem_image]
      refine ⟨k, Finset.mem_Icc.mpr ⟨?_, ?_⟩, rfl⟩
      · rcases Nat.eq_zero_or_pos k with h | h
        · subst h
          rw [mul_zero] at hb
          exact absurd hb hA
        · exact h
      · rw [Nat.le_div_iff_mul_le hxpos, mul_comm]
        exact Finset.le_max' A _ hb
    have hcard : A.card ≤ A.max' ⟨x, hx⟩ / x :=
      calc A.card ≤ _ := Finset.card_le_card hsub
        _ ≤ (Finset.Icc 1 (A.max' ⟨x, hx⟩ / x)).card := Finset.card_image_le
        _ = A.max' ⟨x, hx⟩ / x := by simp
    calc x * A.card ≤ x * (A.max' ⟨x, hx⟩ / x) := Nat.mul_le_mul_left x hcard
      _ ≤ A.max' ⟨x, hx⟩ := Nat.mul_div_le _ x
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-3377fd96».Context

/-! Graham's gcd conjecture (Erdős problem 402) when some element `x` of `A` has no prime factor
below `|A|`: either `x` divides every element, and then the largest element is at least `|A| * x`,
or `gcd(x, b) < x` for some `b`, and then `x / gcd(x, b)` is a divisor of `x` above 1, so at
least `x.minFac ≥ |A|`. Contains the case of a prime `p ≥ |A|` in `A`. -/

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

For a finite set A of positive integers and any x ∈ A whose least prime factor is at least |A|, there are a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. minFac(x) is the least prime factor of x (minFac(1) = 1); the division is in ℚ.

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

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000177.json, merge commit 1ec050140378.

Verdict pass, from attestations/000177.json.

Submitter
t0924-402-http
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/000177.json, merge commit 1ec050140378.

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

theorem witness : ∃ (A : Finset ℕ) (x : ℕ), 0 ∉ A ∧ x ∈ A ∧ A.card ≤ x.minFac :=
  ⟨{2, 3}, 3, by decide, by simp, by rw [Finset.card_pair (by norm_num)]; norm_num⟩

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-3377fd96/Relation.lean, sha256 08273fdbbd2b.
-- 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 → ∀ x ∈ A, A.card ≤ x.minFac →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) := by
  intro h A hA x hx _
  exact h A hA ⟨x, hx⟩

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

x ∈ A is a hypothesis, so A.card ≥ 1 and the rational division is never by zero.

How to read this page

How to read a statement’s page →