Graham's bound for |A| = 4

variant-780e7ade

proved

A partial route to the problem.

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

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

The proof step by step (outline)

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

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.

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-780e7ade/Proof.lean, line 11 at b8a03abbd120 ↗
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-780e7ade/Proof.lean, line 12 at b8a03abbd120 ↗
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₀.
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-780e7ade/Proof.lean, lines 13–16 at b8a03abbd120 ↗
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-780e7ade/Proof.lean, line 17 at b8a03abbd120 ↗
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-780e7ade/Proof.lean, line 18 at b8a03abbd120 ↗
aux have ∀ x ∈ A, x < A.max' hne → (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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 * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne.
Lean, lines 19–48
```
  have aux : ∀ x ∈ A, x < A.max' hne →
      (A.max' hne).gcd x * 4 ≤ A.max' hne ∨ 2 * x = A.max' hne ∨ 3 * x = A.max' hne ∨
        3 * x = 2 * 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 hk4 : 4 ≤ k
    · left
      calc (A.max' hne).gcd x * 4 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk4
        _ = 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 := by omega
      rcases hk' with rfl | rfl
      · have : j = 1 := by omega
        subst this
        omega
      · have : j = 1 ∨ j = 2 := by omega
        rcases this with rfl | rfl <;> omega
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 19–48 at b8a03abbd120 ↗
1. aux.hxpos have (0 : ℕ) < x
  Leaves (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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-780e7ade/Proof.lean, line 23 at b8a03abbd120 ↗
2. aux.s2 obtain (A.max' hne).gcd x ∣ A.max' hne
  Leaves (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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-780e7ade/Proof.lean, line 24 at b8a03abbd120 ↗
3. aux.s3 obtain (A.max' hne).gcd x ∣ x
  Leaves (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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-780e7ade/Proof.lean, line 25 at b8a03abbd120 ↗
4. aux.hgpos have (0 : ℕ) < (A.max' hne).gcd x
  Leaves (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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-780e7ade/Proof.lean, line 26 at b8a03abbd120 ↗
5. aux.s5 case
  Leaves (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne.
  Lean, lines 28–30
  · left calc (A.max' hne).gcd x * 4 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk4 _ = A.max' hne := hk.symm
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 28–30 at b8a03abbd120 ↗
  aux.s5.s1 calc (A.max' hne).gcd x * (4 : ℕ) ≤ (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 * 4 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk4
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 29 at b8a03abbd120 ↗
  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-780e7ade/Proof.lean, line 30 at b8a03abbd120 ↗
6. aux.s6 case
  Leaves (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne ∨ (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne.
  Lean, lines 31–48
  · 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 := by omega rcases hk' with rfl | rfl · have : j = 1 := by omega subst this omega · have : j = 1 ∨ j = 2 := by omega rcases this with rfl | rfl <;> omega
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 31–48 at b8a03abbd120 ↗
  aux.s6.hjk have j < k
  Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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-780e7ade/Proof.lean, lines 32–36 at b8a03abbd120 ↗
  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-780e7ade/Proof.lean, line 35 at b8a03abbd120 ↗
  aux.s6.hj1 have (1 : ℕ) ≤ j
  Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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-780e7ade/Proof.lean, lines 37–41 at b8a03abbd120 ↗
  aux.s6.hj1.s1 case
  Leaves (1 : ℕ) ≤ j.
  Lean, lines 39–40
  · subst h omega
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 39–40 at b8a03abbd120 ↗
  aux.s6.hj1.s2 case
  Leaves (1 : ℕ) ≤ j.
  Lean, line 41
  · exact h
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 41 at b8a03abbd120 ↗
  aux.s6.hk' have k = (2 : ℕ) ∨ k = (3 : ℕ) routine: omega
  Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne, with hk' : k = (2 : ℕ) ∨ k = (3 : ℕ).
  Lean, line 42
  have hk' : k = 2 ∨ k = 3 := by omega
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 42 at b8a03abbd120 ↗
  aux.s6.s4 case
  Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * A.max' hne.
  Lean, lines 44–46
  · have : j = 1 := by omega subst this omega
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 44–46 at b8a03abbd120 ↗
  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, with this : j = (1 : ℕ).
  Lean, line 44
  · have : j = 1 := by omega
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 44 at b8a03abbd120 ↗
  aux.s6.s5 case
  Leaves (2 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = A.max' hne ∨ (3 : ℕ) * x = (2 : ℕ) * 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-780e7ade/Proof.lean, lines 47–48 at b8a03abbd120 ↗
  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, with this : j = (1 : ℕ) ∨ j = (2 : ℕ).
  Lean, line 47
  · have : j = 1 ∨ j = 2 := by omega
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 47 at b8a03abbd120 ↗
win have ∀ x ∈ A, (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with win : ∀ x ∈ A, (A.max' hne).gcd x * (4 : ℕ) ≤ A.max' hne → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro.
Lean, lines 49–51
```
  have win : ∀ x ∈ A, (A.max' hne).gcd x * 4 ≤ A.max' hne →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) :=
    fun x hx h => ⟨_, hM, x, hx, key _ x (by rw [h4]; exact h)⟩
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 49–51 at b8a03abbd120 ↗
fin have ∀ u ∈ A, ∀ v ∈ A, (3 : ℕ) * u = (2 : ℕ) * A.max' hne → (2 : ℕ) * v = A.max' hne → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with fin : ∀ u ∈ A, ∀ v ∈ A, (3 : ℕ) * u = (2 : ℕ) * A.max' hne → (2 : ℕ) * v = A.max' hne → ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro.
Lean, lines 52–59
```
  have fin : ∀ u ∈ A, ∀ v ∈ A, 3 * u = 2 * A.max' hne → 2 * v = A.max' hne →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
    intro u hu v hv hu' hv'
    refine ⟨u, hu, v, hv, key u v ?_⟩
    have hd : u.gcd v ∣ u - v := Nat.dvd_sub (Nat.gcd_dvd_left u v) (Nat.gcd_dvd_right u v)
    have hle : u.gcd v ≤ u - v := Nat.le_of_dvd (by omega) hd
    rw [h4]
    omega
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 52–59 at b8a03abbd120 ↗
1. fin.hd have u.gcd v ∣ u - v
  Leaves u.gcd v * A.card ≤ u, with hd : u.gcd v ∣ u - v.
  Uses library Nat.dvd_sub, Nat.gcd_dvd_left, Nat.gcd_dvd_right.
  Lean, line 56
  have hd : u.gcd v ∣ u - v := Nat.dvd_sub (Nat.gcd_dvd_left u v) (Nat.gcd_dvd_right u v)
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 56 at b8a03abbd120 ↗
2. fin.hle have u.gcd v ≤ u - v
  Leaves u.gcd v * A.card ≤ u, with hle : u.gcd v ≤ u - v.
  Uses library Nat.le_of_dvd.
  Lean, line 57
  have hle : u.gcd v ≤ u - v := Nat.le_of_dvd (by omega) hd
  targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 57 at b8a03abbd120 ↗
he have (A.erase (A.max' hne)).card = (3 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with he : (A.erase (A.max' hne)).card = (3 : ℕ).
Uses library Finset.card_erase_of_mem.
Lean, lines 60–61
```
  have he : (A.erase (A.max' hne)).card = 3 := by
    rw [Finset.card_erase_of_mem hM, h4]
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, lines 60–61 at b8a03abbd120 ↗
s10 obtain ∃ (x : ℕ) (y : ℕ) (z : ℕ), x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ A.erase (A.max' hne) = {x, y, z}
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, y : ℕ, z : ℕ, hxy : x ≠ y, hxz : x ≠ z, hyz : y ≠ z, hexyz : A.erase (A.max' hne) = {x, y, z}.
Uses library Finset.card_eq_three.
Lean, line 62
```
  obtain ⟨x, y, z, hxy, hxz, hyz, hexyz⟩ := Finset.card_eq_three.mp he
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 62 at b8a03abbd120 ↗
hx have x ∈ A.erase (A.max' hne)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hx : x ∈ A.erase (A.max' hne).
Lean, line 63
```
  have hx : x ∈ A.erase (A.max' hne) := by rw [hexyz]; simp
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 63 at b8a03abbd120 ↗
hy have y ∈ A.erase (A.max' hne)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hy : y ∈ A.erase (A.max' hne).
Lean, line 64
```
  have hy : y ∈ A.erase (A.max' hne) := by rw [hexyz]; simp
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 64 at b8a03abbd120 ↗
hz have z ∈ A.erase (A.max' hne)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hz : z ∈ A.erase (A.max' hne).
Lean, line 65
```
  have hz : z ∈ A.erase (A.max' hne) := by rw [hexyz]; simp
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 65 at b8a03abbd120 ↗
hxlt have x < A.max' hne
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hxlt : x < A.max' hne.
Uses library lt_of_le_of_ne, Finset.le_max'.
Lean, line 67
```
  have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 67 at b8a03abbd120 ↗
hylt have y < A.max' hne
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hylt : y < A.max' hne.
Uses library lt_of_le_of_ne, Finset.le_max'.
Lean, line 68
```
  have hylt : y < A.max' hne := lt_of_le_of_ne (Finset.le_max' A y hy.2) hy.1
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 68 at b8a03abbd120 ↗
hzlt have z < A.max' hne
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hzlt : z < A.max' hne.
Uses library lt_of_le_of_ne, Finset.le_max'.
Lean, line 69
```
  have hzlt : z < A.max' hne := lt_of_le_of_ne (Finset.le_max' A z hz.2) hz.1
```
targets/erdos-402/nodes/variant-780e7ade/Proof.lean, line 69 at b8a03abbd120 ↗

The proof in Lean (Proof.lean)

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

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-780e7ade/Proof.lean, sha256 50cea9c21682.

import Mathlib
import Nodes.«variant-780e7ade».Context

/-! Graham's gcd conjecture (Erdős problem 402) for four-element sets: with M the largest
element, if every b had gcd(M, b) > M/4 then every b would be one of M, M/2, M/3, 2M/3, and
the pair 2M/3, M/2 = 4t, 3t has gcd t, which is a quarter of 4t. -/

theorem Opn.erdos_402_card_four :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 4 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A hA h4
  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 * 4 ≤ A.max' hne ∨ 2 * x = A.max' hne ∨ 3 * x = A.max' hne ∨
        3 * x = 2 * 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 hk4 : 4 ≤ k
    · left
      calc (A.max' hne).gcd x * 4 ≤ (A.max' hne).gcd x * k := Nat.mul_le_mul_left _ hk4
        _ = 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 := by omega
      rcases hk' with rfl | rfl
      · have : j = 1 := by omega
        subst this
        omega
      · have : j = 1 ∨ j = 2 := by omega
        rcases this with rfl | rfl <;> omega
  have win : ∀ x ∈ A, (A.max' hne).gcd x * 4 ≤ A.max' hne →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) :=
    fun x hx h => ⟨_, hM, x, hx, key _ x (by rw [h4]; exact h)⟩
  have fin : ∀ u ∈ A, ∀ v ∈ A, 3 * u = 2 * A.max' hne → 2 * v = A.max' hne →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
    intro u hu v hv hu' hv'
    refine ⟨u, hu, v, hv, key u v ?_⟩
    have hd : u.gcd v ∣ u - v := Nat.dvd_sub (Nat.gcd_dvd_left u v) (Nat.gcd_dvd_right u v)
    have hle : u.gcd v ≤ u - v := Nat.le_of_dvd (by omega) hd
    rw [h4]
    omega
  have he : (A.erase (A.max' hne)).card = 3 := by
    rw [Finset.card_erase_of_mem hM, h4]
  obtain ⟨x, y, z, hxy, hxz, hyz, hexyz⟩ := Finset.card_eq_three.mp he
  have hx : x ∈ A.erase (A.max' hne) := by rw [hexyz]; simp
  have hy : y ∈ A.erase (A.max' hne) := by rw [hexyz]; simp
  have hz : z ∈ A.erase (A.max' hne) := by rw [hexyz]; simp
  rw [Finset.mem_erase] at hx hy hz
  have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1
  have hylt : y < A.max' hne := lt_of_le_of_ne (Finset.le_max' A y hy.2) hy.1
  have hzlt : z < A.max' hne := lt_of_le_of_ne (Finset.le_max' A z hz.2) hz.1
  rcases aux x hx.2 hxlt with h1 | h1 | h1 | h1 <;>
  rcases aux y hy.2 hylt with h2 | h2 | h2 | h2 <;>
  rcases aux z hz.2 hzlt with h3 | h3 | h3 | h3 <;>
  first
    | exact win x hx.2 h1
    | exact win y hy.2 h2
    | exact win z hz.2 h3
    | (exfalso; omega)
    | exact fin x hx.2 y hy.2 h1 h2
    | exact fin x hx.2 z hz.2 h1 h3
    | exact fin y hy.2 x hx.2 h2 h1
    | exact fin y hy.2 z hz.2 h2 h3
    | exact fin z hz.2 x hx.2 h3 h1
    | exact fin z hz.2 y hy.2 h3 h2

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-780e7ade».Context

/-! Graham's gcd conjecture (Erdős problem 402) for four-element sets: with M the largest
element, if every b had gcd(M, b) > M/4 then every b would be one of M, M/2, M/3, 2M/3, and
the pair 2M/3, M/2 = 4t, 3t has gcd t, which is a quarter of 4t. -/

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

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| = 4 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$

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

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

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

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000191.json.

Submitter: t0924-402-http
Toolchain: leanprover/lean4:v4.33.1 (hash f54d0bc916bf76a7fae460ce9d078ccd1f74aeb4fd12c4b6546bca28b6aa1c63)
Mathlib: 0df444a360eaa60ab8c11dca51a86af692955474
Reviewer: none needed (calibration)

Step	Check	Result
1	toolchain	pass
2	paths	pass
4	kernel-replay	pass
5	axioms	pass
6	hazards	pass
7	witness	pass
8	deps	pass

Witness

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

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/variant-780e7ade/Witness.lean, sha256 d9597d23e996.

import Mathlib

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 4 :=
  ⟨{1, 2, 3, 4}, 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-780e7ade/Relation.lean, sha256 4579a6a65c46.

-- 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 = 4 → ∃ 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 = 4 is a hypothesis, so the rational division is by 4.

How to read this page

How to read a statement’s page →