Open Proof Network

Problems / erdos-402 / variant-bc28297c

Graham's bound for |A| = 5

variant-bc28297c

proved

A partial route to the problem.

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

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

The proof step by step (outline)

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

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 routine: omega

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

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

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 11 at c7955ccab7df ↗

  2. 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 12
      have hne : A.Nonempty := Finset.card_pos.mp hpos

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 12 at c7955ccab7df ↗

  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 13–16
      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-bc28297c/Proof.lean, lines 13–16 at c7955ccab7df ↗

  4. 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 17
      have hM : A.max' hne ∈ A := Finset.max'_mem A hne

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 17 at c7955ccab7df ↗

  5. 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 18
      have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 18 at c7955ccab7df ↗

  6. aux have ∀ x ∈ A, x < A.max' hne → (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with aux : ∀ x ∈ A, x < A.max' hne → (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

    Lean, lines 19–50
      have aux : ∀ x ∈ A, x < A.max' hne →
      (A.max' hne).gcd x * 5 ≤ A.max' hne ∨ 2 * x = A.max' hne ∨ 3 * x = A.max' hne ∨
        3 * x = 2 * A.max' hne ∨ 4 * x = A.max' hne ∨ 4 * x = 3 * A.max' hne := by
    intro x hx hlt
    have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx))
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
    have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    by_cases hk5 : 5 ≤ k
    · left
      calc (A.max' hne).gcd x * 5 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk5
        _ = A.max' hne := hk.symm
    · right
      have hjk : j < k := by
        by_contra hh
        push_neg at hh
        have : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j := Nat.mul_le_mul_left _ hh
        omega
      have hj1 : 1 ≤ j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · subst h
          omega
        · exact h
      have hk' : k = 2 ∨ k = 3 ∨ k = 4 := by omega
      rcases hk' with rfl | rfl | rfl
      · have : j = 1 := by omega
        subst this
        omega
      · have : j = 1 ∨ j = 2 := by omega
        rcases this with rfl | rfl <;> omega
      · have : j = 1 ∨ j = 2 ∨ j = 3 := by omega
        rcases this with rfl | rfl | rfl <;> omega

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 19–50 at c7955ccab7df ↗

    1. aux.hxpos have (0 : ℕ) < x

      Leaves (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with hxpos : (0 : ℕ) < x.

      Uses library Nat.pos_of_ne_zero.

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

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 23 at c7955ccab7df ↗

    2. aux.s2 obtain (A.max' hne).gcd x ∣ A.max' hne

      Leaves (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with k : ℕ, hk : A.max' hne = (A.max' hne).gcd x * k.

      Uses library Nat.gcd_dvd_left.

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

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 24 at c7955ccab7df ↗

    3. aux.s3 obtain (A.max' hne).gcd x ∣ x

      Leaves (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with j : ℕ, hj : x = (A.max' hne).gcd x * j.

      Uses library Nat.gcd_dvd_right.

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

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 25 at c7955ccab7df ↗

    4. aux.hgpos have (0 : ℕ) < (A.max' hne).gcd x

      Leaves (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with hgpos : (0 : ℕ) < (A.max' hne).gcd x.

      Uses library Nat.gcd_pos_of_pos_right.

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

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 26 at c7955ccab7df ↗

    5. aux.s5 case

      Leaves (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

      Lean, lines 28–30
          · left
      calc (A.max' hne).gcd x * 5 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk5
        _ = A.max' hne := hk.symm

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 28–30 at c7955ccab7df ↗

      1. aux.s5.s1 calc (A.max' hne).gcd x * (5 : ℕ) ≤ (A.max' hne).gcd x * k

        Closes the goal.

        Uses library Nat.mul_le_mul_left.

        Lean, line 29
              calc (A.max' hne).gcd x * 5 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk5

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 29 at c7955ccab7df ↗

      2. aux.s5.s2 calc (A.max' hne).gcd x * k = A.max' hne

        Closes the goal.

        Lean, line 30
                _ = A.max' hne := hk.symm

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 30 at c7955ccab7df ↗

    6. aux.s6 case

      Leaves (A.max' hne).gcd x * (5 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

      Lean, lines 31–50
          · right
      have hjk : j < k := by
        by_contra hh
        push_neg at hh
        have : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j := Nat.mul_le_mul_left _ hh
        omega
      have hj1 : 1 ≤ j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · subst h
          omega
        · exact h
      have hk' : k = 2 ∨ k = 3 ∨ k = 4 := by omega
      rcases hk' with rfl | rfl | rfl
      · have : j = 1 := by omega
        subst this
        omega
      · have : j = 1 ∨ j = 2 := by omega
        rcases this with rfl | rfl <;> omega
      · have : j = 1 ∨ j = 2 ∨ j = 3 := by omega
        rcases this with rfl | rfl | rfl <;> omega

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 31–50 at c7955ccab7df ↗

      1. aux.s6.hjk have j < k

        Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with hjk : j < k.

        Lean, lines 32–36
              have hjk : j < k := by
        by_contra hh
        push_neg at hh
        have : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j := Nat.mul_le_mul_left _ hh
        omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 32–36 at c7955ccab7df ↗

        1. aux.s6.hjk.this have (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j

          Leaves False, with this : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j.

          Uses library Nat.mul_le_mul_left.

          Lean, line 35
                  have : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j := Nat.mul_le_mul_left _ hh

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 35 at c7955ccab7df ↗

      2. aux.s6.hj1 have (1 : ℕ) ≤ j

        Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with hj1 : (1 : ℕ) ≤ j.

        Uses library Nat.eq_zero_or_pos.

        Lean, lines 37–41
              have hj1 : 1 ≤ j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · subst h
          omega
        · exact h

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 37–41 at c7955ccab7df ↗

        1. aux.s6.hj1.s1 case

          Leaves (1 : ℕ) ≤ j.

          Lean, lines 39–40
                  · subst h
          omega

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 39–40 at c7955ccab7df ↗

        2. aux.s6.hj1.s2 case

          Leaves (1 : ℕ) ≤ j.

          Lean, line 41
                  · exact h

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 41 at c7955ccab7df ↗

      3. aux.s6.hk' have k = (2 : ℕ) ∨ k = (3 : ℕ) ∨ k = (4 : ℕ) routine: omega

        Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with hk' : k = (2 : ℕ) ∨ k = (3 : ℕ) ∨ k = (4 : ℕ).

        Lean, line 42
              have hk' : k = 2 ∨ k = 3 ∨ k = 4 := by omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 42 at c7955ccab7df ↗

      4. aux.s6.s4 case

        Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

        Lean, lines 44–46
              · have : j = 1 := by omega
        subst this
        omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 44–46 at c7955ccab7df ↗

        1. aux.s6.s4.this have j = (1 : ℕ) routine: omega

          Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with this : j = (1 : ℕ).

          Lean, line 44
                · have : j = 1 := by omega

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 44 at c7955ccab7df ↗

      5. aux.s6.s5 case

        Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

        Lean, lines 47–48
              · have : j = 1 ∨ j = 2 := by omega
        rcases this with rfl | rfl <;> omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 47–48 at c7955ccab7df ↗

        1. aux.s6.s5.this have j = (1 : ℕ) ∨ j = (2 : ℕ) routine: omega

          Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with this : j = (1 : ℕ) ∨ j = (2 : ℕ).

          Lean, line 47
                · have : j = 1 ∨ j = 2 := by omega

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 47 at c7955ccab7df ↗

      6. aux.s6.s6 case

        Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

        Lean, lines 49–50
              · have : j = 1 ∨ j = 2 ∨ j = 3 := by omega
        rcases this with rfl | rfl | rfl <;> omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 49–50 at c7955ccab7df ↗

        1. aux.s6.s6.this have j = (1 : ℕ) ∨ j = (2 : ℕ) ∨ j = (3 : ℕ) routine: omega

          Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne, with this : j = (1 : ℕ) ∨ j = (2 : ℕ) ∨ j = (3 : ℕ).

          Lean, line 49
                · have : j = 1 ∨ j = 2 ∨ j = 3 := by omega

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 49 at c7955ccab7df ↗

  7. hle have ∀ x ∈ A, x ≠ A.max' hne → x < A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hle : ∀ x ∈ A, x ≠ A.max' hne → x < A.max' hne.

    Uses library lt_of_le_of_ne, Finset.le_max'.

    Lean, lines 51–52
      have hle : ∀ x ∈ A, x ≠ A.max' hne → x < A.max' hne :=
    fun x hx hxM => lt_of_le_of_ne (Finset.le_max' A x hx) hxM

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 51–52 at c7955ccab7df ↗

  8. he have (A.erase (A.max' hne)).card = (4 : ℕ)

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

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

    Lean, lines 53–54
      have he : (A.erase (A.max' hne)).card = 4 := by
    rw [Finset.card_erase_of_mem hM, h5]

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 53–54 at c7955ccab7df ↗

  9. s9 case

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

    Uses library Exists.intro Existential introduction. .

    Lean, lines 56–57
      · obtain ⟨x, hx, -, h⟩ := hw
    exact ⟨_, hM, x, hx, key _ x (by rw [h5]; exact h)⟩

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 56–57 at c7955ccab7df ↗

    1. s9.s1 obtain ∃ x ∈ A, x < A.max' hne ∧ (A.max' hne).gcd x * (5 : ℕ) ≤ 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 * (5 : ℕ) ≤ A.max' hne.

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

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 56 at c7955ccab7df ↗

  10. forms have ∀ x ∈ A, x ≠ A.max' hne → (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with forms : ∀ x ∈ A, x ≠ A.max' hne → (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

    Lean, lines 58–64
      have forms : ∀ x ∈ A, x ≠ A.max' hne →
      2 * x = A.max' hne ∨ 3 * x = A.max' hne ∨ 3 * x = 2 * A.max' hne ∨
        4 * x = A.max' hne ∨ 4 * x = 3 * A.max' hne := by
    intro x hx hxM
    rcases aux x hx (hle x hx hxM) with h | h
    · exact absurd ⟨x, hx, hle x hx hxM, h⟩ hw
    · exact h

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 58–64 at c7955ccab7df ↗

    1. forms.s1 case

      Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

      Uses library absurd Anything follows from two contradictory hypotheses. , Exists.intro Existential introduction. .

      Lean, line 63
          · exact absurd ⟨x, hx, hle x hx hxM, h⟩ hw

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 63 at c7955ccab7df ↗

    2. forms.s2 case

      Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne ∨ (4 : ℕ) * x = A.max' hne ∨ (4 : ℕ) * x = (3 : ℕ) * A.max' hne.

      Lean, line 64
          · exact h

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 64 at c7955ccab7df ↗

  11. gdvd have ∀ (u v c d : ℕ), u.gcd v ∣ c * v - d * u

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with gdvd : ∀ (u v c d : ℕ), u.gcd v ∣ c * v - d * u.

    Uses library Nat.dvd_sub, Dvd.dvd.mul_left Alias of dvd_mul_of_dvd_right. , Nat.gcd_dvd_right, Nat.gcd_dvd_left.

    Lean, lines 65–67
      have gdvd : ∀ u v c d : ℕ, u.gcd v ∣ c * v - d * u := fun u v c d =>
    Nat.dvd_sub (Dvd.dvd.mul_left (Nat.gcd_dvd_right u v) c)
      (Dvd.dvd.mul_left (Nat.gcd_dvd_left u v) d)

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 65–67 at c7955ccab7df ↗

  12. gdvd' have ∀ (u v c d : ℕ), u.gcd v ∣ d * u - c * v

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with gdvd' : ∀ (u v c d : ℕ), u.gcd v ∣ d * u - c * v.

    Uses library Nat.dvd_sub, Dvd.dvd.mul_left Alias of dvd_mul_of_dvd_right. , Nat.gcd_dvd_left, Nat.gcd_dvd_right.

    Lean, lines 68–70
      have gdvd' : ∀ u v c d : ℕ, u.gcd v ∣ d * u - c * v := fun u v c d =>
    Nat.dvd_sub (Dvd.dvd.mul_left (Nat.gcd_dvd_left u v) d)
      (Dvd.dvd.mul_left (Nat.gcd_dvd_right u v) c)

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 68–70 at c7955ccab7df ↗

  13. sub3 have ∀ (p q r : ℕ), (∀ x ∈ A, x ≠ A.max' hne → x = p ∨ x = q ∨ x = r) → False

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with sub3 : ∀ (p q r : ℕ), (∀ x ∈ A, x ≠ A.max' hne → x = p ∨ x = q ∨ x = r) → False.

    Uses library False False is the empty proposition. .

    Lean, lines 71–79
      have sub3 : ∀ p q r : ℕ, (∀ x ∈ A, x ≠ A.max' hne → x = p ∨ x = q ∨ x = r) → False := by
    intro p q r h
    have hs : A.erase (A.max' hne) ⊆ {p, q, r} := by
      intro x hx
      rw [Finset.mem_erase] at hx
      simp only [Finset.mem_insert, Finset.mem_singleton]
      exact h x hx.2 hx.1
    have := (Finset.card_le_card hs).trans Finset.card_le_three
    omega

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 71–79 at c7955ccab7df ↗

    1. sub3.hs have A.erase (A.max' hne) ⊆ {p, q, r}

      Leaves False, with hs : A.erase (A.max' hne) ⊆ {p, q, r}.

      Uses library Finset.mem_erase, Finset.mem_insert, Finset.mem_singleton.

      Lean, lines 73–77
          have hs : A.erase (A.max' hne) ⊆ {p, q, r} := by
      intro x hx
      rw [Finset.mem_erase] at hx
      simp only [Finset.mem_insert, Finset.mem_singleton]
      exact h x hx.2 hx.1

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 73–77 at c7955ccab7df ↗

    2. sub3.this have (A.erase (A.max' hne)).card ≤ (3 : ℕ)

      Leaves False, with this : (A.erase (A.max' hne)).card ≤ (3 : ℕ).

      Uses library Finset.card_le_card, Finset.card_le_three.

      Lean, line 78
          have := (Finset.card_le_card hs).trans Finset.card_le_three

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 78 at c7955ccab7df ↗

  14. s14 case

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

    Lean, lines 81–102
      · obtain ⟨u, hu, hu'⟩ := hE
    by_cases hB : ∃ v ∈ A, 3 * v = A.max' hne
    · obtain ⟨v, hv, hv'⟩ := hB
      refine ⟨u, hu, v, hv, key u v ?_⟩
      have := Nat.le_of_dvd (by omega) (gdvd' u v 2 1)
      rw [h5]
      omega
    by_cases hC : ∃ v ∈ A, 3 * v = 2 * A.max' hne
    · obtain ⟨v, hv, hv'⟩ := hC
      refine ⟨u, hu, v, hv, key u v ?_⟩
      have := Nat.le_of_dvd (by omega) (gdvd' u v 1 1)
      rw [h5]
      omega
    exfalso
    refine sub3 (A.max' hne / 2) (A.max' hne / 4) (3 * A.max' hne / 4) ?_
    intro x hx hxM
    rcases forms x hx hxM with h | h | h | h | h
    · omega
    · exact absurd ⟨x, hx, h⟩ hB
    · exact absurd ⟨x, hx, h⟩ hC
    · omega
    · omega

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 81–102 at c7955ccab7df ↗

    1. s14.s1 obtain ∃ u ∈ A, (4 : ℕ) * u = (3 : ℕ) * A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with u : ℕ, hu : u ∈ A, hu' : (4 : ℕ) * u = (3 : ℕ) * A.max' hne.

      Lean, line 81
        · obtain ⟨u, hu, hu'⟩ := hE

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 81 at c7955ccab7df ↗

    2. s14.s2 case

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

      Uses library Exists.intro Existential introduction. .

      Lean, lines 83–87
          · obtain ⟨v, hv, hv'⟩ := hB
      refine ⟨u, hu, v, hv, key u v ?_⟩
      have := Nat.le_of_dvd (by omega) (gdvd' u v 2 1)
      rw [h5]
      omega

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 83–87 at c7955ccab7df ↗

      1. s14.s2.s1 obtain ∃ v ∈ A, (3 : ℕ) * v = A.max' hne

        Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with v : ℕ, hv : v ∈ A, hv' : (3 : ℕ) * v = A.max' hne.

        Lean, line 83
            · obtain ⟨v, hv, hv'⟩ := hB

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 83 at c7955ccab7df ↗

      2. s14.s2.this have u.gcd v ≤ (1 : ℕ) * u - (2 : ℕ) * v

        Leaves u.gcd v * A.card ≤ u, with this : u.gcd v ≤ (1 : ℕ) * u - (2 : ℕ) * v.

        Uses library Nat.le_of_dvd.

        Lean, line 85
              have := Nat.le_of_dvd (by omega) (gdvd' u v 2 1)

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 85 at c7955ccab7df ↗

    3. s14.s3 case

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

      Uses library Exists.intro Existential introduction. .

      Lean, lines 89–93
          · obtain ⟨v, hv, hv'⟩ := hC
      refine ⟨u, hu, v, hv, key u v ?_⟩
      have := Nat.le_of_dvd (by omega) (gdvd' u v 1 1)
      rw [h5]
      omega

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 89–93 at c7955ccab7df ↗

      1. s14.s3.s1 obtain ∃ v ∈ A, (3 : ℕ) * v = (2 : ℕ) * A.max' hne

        Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with v : ℕ, hv : v ∈ A, hv' : (3 : ℕ) * v = (2 : ℕ) * A.max' hne.

        Lean, line 89
            · obtain ⟨v, hv, hv'⟩ := hC

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 89 at c7955ccab7df ↗

      2. s14.s3.this have u.gcd v ≤ (1 : ℕ) * u - (1 : ℕ) * v

        Leaves u.gcd v * A.card ≤ u, with this : u.gcd v ≤ (1 : ℕ) * u - (1 : ℕ) * v.

        Uses library Nat.le_of_dvd.

        Lean, line 91
              have := Nat.le_of_dvd (by omega) (gdvd' u v 1 1)

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 91 at c7955ccab7df ↗

    4. s14.s4 case routine: omega

      Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (4 : ℕ) ∨ x = (3 : ℕ) * A.max' hne / (4 : ℕ).

      Lean, line 98
          · omega

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 98 at c7955ccab7df ↗

    5. s14.s5 case

      Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (4 : ℕ) ∨ x = (3 : ℕ) * A.max' hne / (4 : ℕ).

      Uses library absurd Anything follows from two contradictory hypotheses. , Exists.intro Existential introduction. .

      Lean, line 99
          · exact absurd ⟨x, hx, h⟩ hB

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 99 at c7955ccab7df ↗

    6. s14.s6 case

      Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (4 : ℕ) ∨ x = (3 : ℕ) * A.max' hne / (4 : ℕ).

      Uses library absurd Anything follows from two contradictory hypotheses. , Exists.intro Existential introduction. .

      Lean, line 100
          · exact absurd ⟨x, hx, h⟩ hC

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 100 at c7955ccab7df ↗

    7. s14.s7 case routine: omega

      Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (4 : ℕ) ∨ x = (3 : ℕ) * A.max' hne / (4 : ℕ).

      Lean, line 101
          · omega

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 101 at c7955ccab7df ↗

    8. s14.s8 case routine: omega

      Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (4 : ℕ) ∨ x = (3 : ℕ) * A.max' hne / (4 : ℕ).

      Lean, line 102
          · omega

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 102 at c7955ccab7df ↗

  15. s15 case

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

    Lean, lines 103–128
      · by_cases hC : ∃ u ∈ A, 3 * u = 2 * A.max' hne
    · obtain ⟨u, hu, hu'⟩ := hC
      by_cases hD : ∃ v ∈ A, 4 * v = A.max' hne
      · obtain ⟨v, hv, hv'⟩ := hD
        refine ⟨u, hu, v, hv, key u v ?_⟩
        have := Nat.le_of_dvd (by omega) (gdvd u v 3 1)
        rw [h5]
        omega
      exfalso
      refine sub3 (A.max' hne / 2) (A.max' hne / 3) (2 * A.max' hne / 3) ?_
      intro x hx hxM
      rcases forms x hx hxM with h | h | h | h | h
      · omega
      · omega
      · omega
      · exact absurd ⟨x, hx, h⟩ hD
      · exact absurd ⟨x, hx, h⟩ hE
    · exfalso
      refine sub3 (A.max' hne / 2) (A.max' hne / 3) (A.max' hne / 4) ?_
      intro x hx hxM
      rcases forms x hx hxM with h | h | h | h | h
      · omega
      · omega
      · exact absurd ⟨x, hx, h⟩ hC
      · omega
      · exact absurd ⟨x, hx, h⟩ hE

    targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 103–128 at c7955ccab7df ↗

    1. s15.s1 case

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

      Lean, lines 104–119
          · obtain ⟨u, hu, hu'⟩ := hC
      by_cases hD : ∃ v ∈ A, 4 * v = A.max' hne
      · obtain ⟨v, hv, hv'⟩ := hD
        refine ⟨u, hu, v, hv, key u v ?_⟩
        have := Nat.le_of_dvd (by omega) (gdvd u v 3 1)
        rw [h5]
        omega
      exfalso
      refine sub3 (A.max' hne / 2) (A.max' hne / 3) (2 * A.max' hne / 3) ?_
      intro x hx hxM
      rcases forms x hx hxM with h | h | h | h | h
      · omega
      · omega
      · omega
      · exact absurd ⟨x, hx, h⟩ hD
      · exact absurd ⟨x, hx, h⟩ hE

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 104–119 at c7955ccab7df ↗

      1. s15.s1.s1 obtain ∃ u ∈ A, (3 : ℕ) * u = (2 : ℕ) * A.max' hne

        Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with u : ℕ, hu : u ∈ A, hu' : (3 : ℕ) * u = (2 : ℕ) * A.max' hne.

        Lean, line 104
            · obtain ⟨u, hu, hu'⟩ := hC

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 104 at c7955ccab7df ↗

      2. s15.s1.s2 case

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

        Uses library Exists.intro Existential introduction. .

        Lean, lines 106–110
              · obtain ⟨v, hv, hv'⟩ := hD
        refine ⟨u, hu, v, hv, key u v ?_⟩
        have := Nat.le_of_dvd (by omega) (gdvd u v 3 1)
        rw [h5]
        omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 106–110 at c7955ccab7df ↗

        1. s15.s1.s2.s1 obtain ∃ v ∈ A, (4 : ℕ) * v = A.max' hne

          Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with v : ℕ, hv : v ∈ A, hv' : (4 : ℕ) * v = A.max' hne.

          Lean, line 106
                · obtain ⟨v, hv, hv'⟩ := hD

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 106 at c7955ccab7df ↗

        2. s15.s1.s2.this have u.gcd v ≤ (3 : ℕ) * v - (1 : ℕ) * u

          Leaves u.gcd v * A.card ≤ u, with this : u.gcd v ≤ (3 : ℕ) * v - (1 : ℕ) * u.

          Uses library Nat.le_of_dvd.

          Lean, line 108
                  have := Nat.le_of_dvd (by omega) (gdvd u v 3 1)

          targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 108 at c7955ccab7df ↗

      3. s15.s1.s3 case routine: omega

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = (2 : ℕ) * A.max' hne / (3 : ℕ).

        Lean, line 115
              · omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 115 at c7955ccab7df ↗

      4. s15.s1.s4 case routine: omega

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = (2 : ℕ) * A.max' hne / (3 : ℕ).

        Lean, line 116
              · omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 116 at c7955ccab7df ↗

      5. s15.s1.s5 case routine: omega

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = (2 : ℕ) * A.max' hne / (3 : ℕ).

        Lean, line 117
              · omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 117 at c7955ccab7df ↗

      6. s15.s1.s6 case

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = (2 : ℕ) * A.max' hne / (3 : ℕ).

        Uses library absurd Anything follows from two contradictory hypotheses. , Exists.intro Existential introduction. .

        Lean, line 118
              · exact absurd ⟨x, hx, h⟩ hD

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 118 at c7955ccab7df ↗

      7. s15.s1.s7 case

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = (2 : ℕ) * A.max' hne / (3 : ℕ).

        Uses library absurd Anything follows from two contradictory hypotheses. , Exists.intro Existential introduction. .

        Lean, line 119
              · exact absurd ⟨x, hx, h⟩ hE

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 119 at c7955ccab7df ↗

    2. s15.s2 case

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

      Lean, lines 120–128
          · exfalso
      refine sub3 (A.max' hne / 2) (A.max' hne / 3) (A.max' hne / 4) ?_
      intro x hx hxM
      rcases forms x hx hxM with h | h | h | h | h
      · omega
      · omega
      · exact absurd ⟨x, hx, h⟩ hC
      · omega
      · exact absurd ⟨x, hx, h⟩ hE

      targets/erdos-402/nodes/variant-bc28297c/Proof.lean, lines 120–128 at c7955ccab7df ↗

      1. s15.s2.s1 case routine: omega

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = A.max' hne / (4 : ℕ).

        Lean, line 124
              · omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 124 at c7955ccab7df ↗

      2. s15.s2.s2 case routine: omega

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = A.max' hne / (4 : ℕ).

        Lean, line 125
              · omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 125 at c7955ccab7df ↗

      3. s15.s2.s3 case

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = A.max' hne / (4 : ℕ).

        Uses library absurd Anything follows from two contradictory hypotheses. , Exists.intro Existential introduction. .

        Lean, line 126
              · exact absurd ⟨x, hx, h⟩ hC

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 126 at c7955ccab7df ↗

      4. s15.s2.s4 case routine: omega

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = A.max' hne / (4 : ℕ).

        Lean, line 127
              · omega

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 127 at c7955ccab7df ↗

      5. s15.s2.s5 case

        Leaves x = A.max' hne / (2 : ℕ) ∨ x = A.max' hne / (3 : ℕ) ∨ x = A.max' hne / (4 : ℕ).

        Uses library absurd Anything follows from two contradictory hypotheses. , Exists.intro Existential introduction. .

        Lean, line 128
              · exact absurd ⟨x, hx, h⟩ hE

        targets/erdos-402/nodes/variant-bc28297c/Proof.lean, line 128 at c7955ccab7df ↗

The proof in Lean (Proof.lean)

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

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

/-! Graham's gcd conjecture (Erdős problem 402) for five-element sets: with M the largest
element, if every b had gcd(M, b) > M/5 then every b would be (j/k)M with j ≤ k ≤ 4, and any
five of those six values contain a pair 9s, 8s or 8s, 3s or 9s, 4s whose gcd is s. -/

theorem Opn.erdos_402_card_five :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 5 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A hA h5
  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))
  have aux : ∀ x ∈ A, x < A.max' hne →
      (A.max' hne).gcd x * 5 ≤ A.max' hne ∨ 2 * x = A.max' hne ∨ 3 * x = A.max' hne ∨
        3 * x = 2 * A.max' hne ∨ 4 * x = A.max' hne ∨ 4 * x = 3 * A.max' hne := by
    intro x hx hlt
    have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx))
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
    have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    by_cases hk5 : 5 ≤ k
    · left
      calc (A.max' hne).gcd x * 5 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk5
        _ = A.max' hne := hk.symm
    · right
      have hjk : j < k := by
        by_contra hh
        push_neg at hh
        have : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j := Nat.mul_le_mul_left _ hh
        omega
      have hj1 : 1 ≤ j := by
        rcases Nat.eq_zero_or_pos j with h | h
        · subst h
          omega
        · exact h
      have hk' : k = 2 ∨ k = 3 ∨ k = 4 := by omega
      rcases hk' with rfl | rfl | rfl
      · have : j = 1 := by omega
        subst this
        omega
      · have : j = 1 ∨ j = 2 := by omega
        rcases this with rfl | rfl <;> omega
      · have : j = 1 ∨ j = 2 ∨ j = 3 := by omega
        rcases this with rfl | rfl | rfl <;> omega
  have hle : ∀ x ∈ A, x ≠ A.max' hne → x < A.max' hne :=
    fun x hx hxM => lt_of_le_of_ne (Finset.le_max' A x hx) hxM
  have he : (A.erase (A.max' hne)).card = 4 := by
    rw [Finset.card_erase_of_mem hM, h5]
  by_cases hw : ∃ x ∈ A, x < A.max' hne ∧ (A.max' hne).gcd x * 5 ≤ A.max' hne
  · obtain ⟨x, hx, -, h⟩ := hw
    exact ⟨_, hM, x, hx, key _ x (by rw [h5]; exact h)⟩
  have forms : ∀ x ∈ A, x ≠ A.max' hne →
      2 * x = A.max' hne ∨ 3 * x = A.max' hne ∨ 3 * x = 2 * A.max' hne ∨
        4 * x = A.max' hne ∨ 4 * x = 3 * A.max' hne := by
    intro x hx hxM
    rcases aux x hx (hle x hx hxM) with h | h
    · exact absurd ⟨x, hx, hle x hx hxM, h⟩ hw
    · exact h
  have gdvd : ∀ u v c d : ℕ, u.gcd v ∣ c * v - d * u := fun u v c d =>
    Nat.dvd_sub (Dvd.dvd.mul_left (Nat.gcd_dvd_right u v) c)
      (Dvd.dvd.mul_left (Nat.gcd_dvd_left u v) d)
  have gdvd' : ∀ u v c d : ℕ, u.gcd v ∣ d * u - c * v := fun u v c d =>
    Nat.dvd_sub (Dvd.dvd.mul_left (Nat.gcd_dvd_left u v) d)
      (Dvd.dvd.mul_left (Nat.gcd_dvd_right u v) c)
  have sub3 : ∀ p q r : ℕ, (∀ x ∈ A, x ≠ A.max' hne → x = p ∨ x = q ∨ x = r) → False := by
    intro p q r h
    have hs : A.erase (A.max' hne) ⊆ {p, q, r} := by
      intro x hx
      rw [Finset.mem_erase] at hx
      simp only [Finset.mem_insert, Finset.mem_singleton]
      exact h x hx.2 hx.1
    have := (Finset.card_le_card hs).trans Finset.card_le_three
    omega
  by_cases hE : ∃ u ∈ A, 4 * u = 3 * A.max' hne
  · obtain ⟨u, hu, hu'⟩ := hE
    by_cases hB : ∃ v ∈ A, 3 * v = A.max' hne
    · obtain ⟨v, hv, hv'⟩ := hB
      refine ⟨u, hu, v, hv, key u v ?_⟩
      have := Nat.le_of_dvd (by omega) (gdvd' u v 2 1)
      rw [h5]
      omega
    by_cases hC : ∃ v ∈ A, 3 * v = 2 * A.max' hne
    · obtain ⟨v, hv, hv'⟩ := hC
      refine ⟨u, hu, v, hv, key u v ?_⟩
      have := Nat.le_of_dvd (by omega) (gdvd' u v 1 1)
      rw [h5]
      omega
    exfalso
    refine sub3 (A.max' hne / 2) (A.max' hne / 4) (3 * A.max' hne / 4) ?_
    intro x hx hxM
    rcases forms x hx hxM with h | h | h | h | h
    · omega
    · exact absurd ⟨x, hx, h⟩ hB
    · exact absurd ⟨x, hx, h⟩ hC
    · omega
    · omega
  · by_cases hC : ∃ u ∈ A, 3 * u = 2 * A.max' hne
    · obtain ⟨u, hu, hu'⟩ := hC
      by_cases hD : ∃ v ∈ A, 4 * v = A.max' hne
      · obtain ⟨v, hv, hv'⟩ := hD
        refine ⟨u, hu, v, hv, key u v ?_⟩
        have := Nat.le_of_dvd (by omega) (gdvd u v 3 1)
        rw [h5]
        omega
      exfalso
      refine sub3 (A.max' hne / 2) (A.max' hne / 3) (2 * A.max' hne / 3) ?_
      intro x hx hxM
      rcases forms x hx hxM with h | h | h | h | h
      · omega
      · omega
      · omega
      · exact absurd ⟨x, hx, h⟩ hD
      · exact absurd ⟨x, hx, h⟩ hE
    · exfalso
      refine sub3 (A.max' hne / 2) (A.max' hne / 3) (A.max' hne / 4) ?_
      intro x hx hxM
      rcases forms x hx hxM with h | h | h | h | h
      · omega
      · omega
      · exact absurd ⟨x, hx, h⟩ hC
      · omega
      · exact absurd ⟨x, hx, h⟩ hE

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

/-! Graham's gcd conjecture (Erdős problem 402) for five-element sets: with M the largest
element, if every b had gcd(M, b) > M/5 then every b would be (j/k)M with j ≤ k ≤ 4, and any
five of those six values contain a pair 9s, 8s or 8s, 3s or 9s, 4s whose gcd is s. -/

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

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

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

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

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000192.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/000192.json, merge commit c7955ccab7df.

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

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 5 :=
  ⟨{1, 2, 3, 4, 5}, by decide, by decide⟩

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-bc28297c/Relation.lean, sha256 76d34961096a.
-- 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 = 5 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) := by
  intro h A hA hc
  exact 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

A.card = 5 is a hypothesis, so the rational division is by 5.

How to read this page

How to read a statement’s page →