Graham's bound for |A| = 10

variant-a5969ff3

proved

A partial route to the problem.

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

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

The proof step by step (outline)

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

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.

red have ∀ (a b : ℕ), (10 : ℕ) * a.gcd b ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with red : ∀ (a b : ℕ), (10 : ℕ) * a.gcd b ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library le_div_iff₀.
Lean, lines 13–16
```
  have red : ∀ a b : ℕ, 10 * a.gcd b ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
    intro a b h
    rw [hcard, le_div_iff₀ (by norm_num)]
    exact_mod_cast (by omega : a.gcd b * 10 ≤ a)
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 13–16 at b48e57a81803 ↗
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 17
```
  have hne : A.Nonempty := Finset.card_pos.mp (by omega)
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 17 at b48e57a81803 ↗
s3 obtain ∃ M ∈ A, ∀ x ∈ A, x ≤ M
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with M : ℕ, hMA : M ∈ A, hMmax : ∀ x ∈ A, x ≤ M.
Uses library Exists.intro.
Lean, lines 18–19
```
  obtain ⟨M, hMA, hMmax⟩ : ∃ M ∈ A, ∀ x ∈ A, x ≤ M :=
    ⟨A.max' hne, A.max'_mem hne, fun x hx => A.le_max' x hx⟩
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 18–19 at b48e57a81803 ↗
hMpos have (0 : ℕ) < M
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hMpos : (0 : ℕ) < M.
Uses library Nat.pos_of_ne_zero.
Lean, line 20
```
  have hMpos : 0 < M := Nat.pos_of_ne_zero (by rintro rfl; exact h0 hMA)
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 20 at b48e57a81803 ↗
s5 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro.
Lean, lines 22–23
```
  · obtain ⟨x, hx, h⟩ := hsmall
    exact ⟨M, hMA, x, hx, red M x h⟩
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 22–23 at b48e57a81803 ↗
1. s5.s1 obtain ∃ x ∈ A, (10 : ℕ) * M.gcd x ≤ M
  Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A, h : (10 : ℕ) * M.gcd x ≤ M.
  Lean, line 22
  · obtain ⟨x, hx, h⟩ := hsmall
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 22 at b48e57a81803 ↗
hval have printed form did not read back: shown as its Lean lines only
```
  have hval : ∀ x ∈ A.erase M, ∃ v ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), 2520 * x = v * M := by
    intro x hx
    obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero (by rintro rfl; exact h0 hxA)
    have hlt : x < M := lt_of_le_of_ne (hMmax x hxA) hxM
    have hbig : M < 10 * M.gcd x := hsmall x hxA
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left M x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right M x
    have hk10 : k < 10 := by
      by_contra hh
      have : M.gcd x * 10 ≤ M.gcd x * k := Nat.mul_le_mul_left _ (by omega)
      omega
    have hjk : j < k := by
      have : M.gcd x * j < M.gcd x * k := by omega
      exact Nat.lt_of_mul_lt_mul_left this
    have hj0 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · rw [h, Nat.mul_zero] at hj; omega
      · exact h
    refine ⟨2520 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 26–47 at b48e57a81803 ↗
1. hval.s1 obtain printed form did not read back: shown as its Lean lines only
  obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 28 at b48e57a81803 ↗
2. hval.hxpos have printed form did not read back: shown as its Lean lines only
  have hxpos : 0 < x := Nat.pos_of_ne_zero (by rintro rfl; exact h0 hxA)
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 29 at b48e57a81803 ↗
3. hval.hlt have printed form did not read back: shown as its Lean lines only
  have hlt : x < M := lt_of_le_of_ne (hMmax x hxA) hxM
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 30 at b48e57a81803 ↗
4. hval.hbig have printed form did not read back: shown as its Lean lines only
  have hbig : M < 10 * M.gcd x := hsmall x hxA
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 31 at b48e57a81803 ↗
5. hval.s5 obtain printed form did not read back: shown as its Lean lines only
  obtain ⟨k, hk⟩ := Nat.gcd_dvd_left M x
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 32 at b48e57a81803 ↗
6. hval.s6 obtain printed form did not read back: shown as its Lean lines only
  obtain ⟨j, hj⟩ := Nat.gcd_dvd_right M x
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 33 at b48e57a81803 ↗
7. hval.hk10 have printed form did not read back: shown as its Lean lines only
  have hk10 : k < 10 := by by_contra hh have : M.gcd x * 10 ≤ M.gcd x * k := Nat.mul_le_mul_left _ (by omega) omega
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 34–37 at b48e57a81803 ↗
  hval.hk10.this have M.gcd x * (10 : ℕ) ≤ M.gcd x * k
  Leaves False, with this : M.gcd x * (10 : ℕ) ≤ M.gcd x * k.
  Uses library Nat.mul_le_mul_left.
  Lean, line 36
  have : M.gcd x * 10 ≤ M.gcd x * k := Nat.mul_le_mul_left _ (by omega)
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 36 at b48e57a81803 ↗
8. hval.hjk have printed form did not read back: shown as its Lean lines only
  have hjk : j < k := by have : M.gcd x * j < M.gcd x * k := by omega exact Nat.lt_of_mul_lt_mul_left this
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 38–40 at b48e57a81803 ↗
  hval.hjk.this have M.gcd x * j < M.gcd x * k routine: omega
  Leaves j < k, with this : M.gcd x * j < M.gcd x * k.
  Lean, line 39
  have : M.gcd x * j < M.gcd x * k := by omega
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 39 at b48e57a81803 ↗
9. hval.hj0 have printed form did not read back: shown as its Lean lines only
  have hj0 : 0 < j := by rcases Nat.eq_zero_or_pos j with h | h · rw [h, Nat.mul_zero] at hj; omega · exact h
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 41–44 at b48e57a81803 ↗
  hval.hj0.s1 case
  Leaves (0 : ℕ) < j.
  Uses library Nat.mul_zero.
  Lean, line 43
  · rw [h, Nat.mul_zero] at hj; omega
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 43 at b48e57a81803 ↗
  hval.hj0.s2 case
  Leaves (0 : ℕ) < j.
  Lean, line 44
  · exact h
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 44 at b48e57a81803 ↗
10. hval.s10 case printed form did not read back: shown as its Lean lines only
  · interval_cases k <;> interval_cases j <;> decide
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 46 at b48e57a81803 ↗
11. hval.s11 case
  Leaves (2520 : ℕ) * x = (2520 : ℕ) * j / k * M.
  Lean, line 47
  · interval_cases k <;> interval_cases j <;> omega
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 47 at b48e57a81803 ↗

hcol have printed form did not read back: shown as its Lean lines only

  have hcol : ∀ v ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) v < 8 := by decide

targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 49 at b48e57a81803 ↗

hgood have printed form did not read back: shown as its Lean lines only

  have hgood : ∀ v ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), ∀ w ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), v ≠ w → (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) v = (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) w →
      10 * v.gcd w ≤ v ∨ 10 * v.gcd w ≤ w := by decide

targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 50–51 at b48e57a81803 ↗

hmaps have ∀ x ∈ A.erase M, (fun (a : ℕ) => if a = (280 : ℕ) then (4 : ℕ) else if a = (315 : ℕ) then (6 : ℕ) else if a = (360 : ℕ) then (2 : ℕ) else if a = (420 : ℕ) then (5 : ℕ) else if a = (504 : ℕ) then (7 : ℕ) else if a = (560 : ℕ) then (6 : ℕ) else if a = (630 : ℕ) then (3 : ℕ) else if a = (720 : ℕ) then (5 : ℕ) else if a = (840 : ℕ) then (1 : ℕ) else if a = (945 : ℕ) then (2 : ℕ) else if a = (1008 : ℕ) then (4 : ℕ) else if a = (1080 : ℕ) then (3 : ℕ) else if a = (1120 : ℕ) then (3 : ℕ) else if a = (1260 : ℕ) then (0 : ℕ) else if a = (1400 : ℕ) then (0 : ℕ) else if a = (1440 : ℕ) then (4 : ℕ) else if a = (1512 : ℕ) then (5 : ℕ) else if a = (1575 : ℕ) then (5 : ℕ) else if a = (1680 : ℕ) then (2 : ℕ) else if a = (1800 : ℕ) then (1 : ℕ) else if a = (1890 : ℕ) then (4 : ℕ) else (truncated)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase M, (fun (a : ℕ) => if a = (280 : ℕ) then (4 : ℕ) else if a = (315 : ℕ) then (6 : ℕ) else if a = (360 : ℕ) then (2 : ℕ) else if a = (420 : ℕ) then (5 : ℕ) else if a = (504 : ℕ) then (7 : ℕ) else if a = (560 : ℕ) then (6 : ℕ) else if a = (630 : ℕ) then (3 : ℕ) else if a = (720 : ℕ) then (5 : ℕ) else if a = (840 : ℕ) then (1 : ℕ) else if a = (945 : ℕ) then (2 : ℕ) else if a = (1008 : ℕ) then (4 : ℕ) else if a = (1080 : ℕ) then (3 : ℕ) else if a = (1120 : ℕ) then (3 : ℕ) else if a = (1260 : ℕ) then (0 : ℕ) else if a = (1400 : ℕ) then (0 : ℕ) else if a = (1440 : ℕ) then (4 : ℕ) else if a = (1512 : ℕ) then (5 : ℕ) else if a = (1575 : ℕ) then (5 : ℕ) else if a = (1680 : ℕ) then (2 : ℕ) else if a = (1800 : ℕ) then (1 : ℕ) else if a = (1890 : ℕ) then (4 : ℕ) else (truncated).
Uses library Finset.range, Finset.mem_range, Nat.mul_div_cancel.
Lean, lines 52–56
```
  have hmaps : ∀ x ∈ A.erase M, (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) (2520 * x / M) ∈ Finset.range 8 := by
    intro x hx
    obtain ⟨v, hv, hxv⟩ := hval x hx
    rw [Finset.mem_range, hxv, Nat.mul_div_cancel _ hMpos]
    exact hcol v hv
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 52–56 at b48e57a81803 ↗
1. hmaps.s1 obtain printed form did not read back: shown as its Lean lines only
  obtain ⟨v, hv, hxv⟩ := hval x hx
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 54 at b48e57a81803 ↗
h9 have (A.erase M).card = (9 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with h9 : (A.erase M).card = (9 : ℕ).
Uses library Finset.card_erase_of_mem.
Lean, line 57
```
  have h9 : (A.erase M).card = 9 := by rw [Finset.card_erase_of_mem hMA, hcard]
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 57 at b48e57a81803 ↗
s11 obtain ∃ x ∈ A.erase M, ∃ y ∈ A.erase M, x ≠ y ∧ (fun (a : ℕ) => if a = (280 : ℕ) then (4 : ℕ) else if a = (315 : ℕ) then (6 : ℕ) else if a = (360 : ℕ) then (2 : ℕ) else if a = (420 : ℕ) then (5 : ℕ) else if a = (504 : ℕ) then (7 : ℕ) else if a = (560 : ℕ) then (6 : ℕ) else if a = (630 : ℕ) then (3 : ℕ) else if a = (720 : ℕ) then (5 : ℕ) else if a = (840 : ℕ) then (1 : ℕ) else if a = (945 : ℕ) then (2 : ℕ) else if a = (1008 : ℕ) then (4 : ℕ) else if a = (1080 : ℕ) then (3 : ℕ) else if a = (1120 : ℕ) then (3 : ℕ) else if a = (1260 : ℕ) then (0 : ℕ) else if a = (1400 : ℕ) then (0 : ℕ) else if a = (1440 : ℕ) then (4 : ℕ) else if a = (1512 : ℕ) then (5 : ℕ) else if a = (1575 : ℕ) then (5 : ℕ) else if a = (1680 : ℕ) then (2 : ℕ) else if a = (1800 : ℕ) then (1 : ℕ) (truncated)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A.erase M, y : ℕ, hy : y ∈ A.erase M, hxy : x ≠ y, hc : (fun (a : ℕ) => if a = (280 : ℕ) then (4 : ℕ) else if a = (315 : ℕ) then (6 : ℕ) else if a = (360 : ℕ) then (2 : ℕ) else if a = (420 : ℕ) then (5 : ℕ) else if a = (504 : ℕ) then (7 : ℕ) else if a = (560 : ℕ) then (6 : ℕ) else if a = (630 : ℕ) then (3 : ℕ) else if a = (720 : ℕ) then (5 : ℕ) else if a = (840 : ℕ) then (1 : ℕ) else if a = (945 : ℕ) then (2 : ℕ) else if a = (1008 : ℕ) then (4 : ℕ) else if a = (1080 : ℕ) then (3 : ℕ) else if a = (1120 : ℕ) then (3 : ℕ) else if a = (1260 : ℕ) then (0 : ℕ) else if a = (1400 : ℕ) then (0 : ℕ) else if a = (1440 : ℕ) then (4 : ℕ) else if a = (1512 : ℕ) then (5 : ℕ) else if a = (1575 : ℕ) then (5 : ℕ) else if a = (1680 : ℕ) then (2 : ℕ) else if a = (1800 : ℕ) then (1 : ℕ) else if a = (1890 : ℕ) then (4 : ℕ) else if a = (1960 : ℕ) then (5 : ℕ) else (truncated).
Uses library Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.card_range.
Lean, lines 58–59
```
  obtain ⟨x, hx, y, hy, hxy, hc⟩ :=
    Finset.exists_ne_map_eq_of_card_lt_of_maps_to (by rw [h9, Finset.card_range]; omega) hmaps
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 58–59 at b48e57a81803 ↗
s12 obtain printed form did not read back: shown as its Lean lines only
```
  obtain ⟨v, hv, hxv⟩ := hval x hx
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 60 at b48e57a81803 ↗
s13 obtain printed form did not read back: shown as its Lean lines only
```
  obtain ⟨w, hw, hyw⟩ := hval y hy
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 61 at b48e57a81803 ↗
hvw have v ≠ w
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hvw : v ≠ w.
Lean, lines 63–65
```
  have hvw : v ≠ w := by
    rintro rfl
    exact hxy (by omega)
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 63–65 at b48e57a81803 ↗
hg have v.gcd w * M = (2520 : ℕ) * x.gcd y
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hg : v.gcd w * M = (2520 : ℕ) * x.gcd y.
Uses library Nat.gcd_mul_right, Nat.gcd_mul_left.
Lean, lines 66–67
```
  have hg : v.gcd w * M = 2520 * x.gcd y := by
    rw [← Nat.gcd_mul_right, ← hxv, ← hyw, Nat.gcd_mul_left]
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 66–67 at b48e57a81803 ↗
hxA have x ∈ A
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hxA : x ∈ A.
Uses library Finset.mem_erase.
Lean, line 68
```
  have hxA := (Finset.mem_erase.mp hx).2
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 68 at b48e57a81803 ↗
hyA have y ∈ A
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hyA : y ∈ A.
Uses library Finset.mem_erase.
Lean, line 69
```
  have hyA := (Finset.mem_erase.mp hy).2
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, line 69 at b48e57a81803 ↗
s18 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro.
Lean, lines 71–73
```
  · have h2 : 10 * (v.gcd w * M) ≤ v * M := by
      rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right M h
    exact ⟨x, hxA, y, hyA, red x y (by omega)⟩
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 71–73 at b48e57a81803 ↗
1. s18.h2 have (10 : ℕ) * (v.gcd w * M) ≤ v * M
  Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with h2 : (10 : ℕ) * (v.gcd w * M) ≤ v * M.
  Uses library Nat.mul_assoc, Nat.mul_le_mul_right.
  Lean, lines 71–72
  · have h2 : 10 * (v.gcd w * M) ≤ v * M := by rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right M h
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 71–72 at b48e57a81803 ↗
s19 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro, Nat.gcd_comm.
Lean, lines 74–76
```
  · have h2 : 10 * (v.gcd w * M) ≤ w * M := by
      rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right M h
    exact ⟨y, hyA, x, hxA, red y x (by rw [Nat.gcd_comm]; omega)⟩
```
targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 74–76 at b48e57a81803 ↗
1. s19.h2 have (10 : ℕ) * (v.gcd w * M) ≤ w * M
  Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with h2 : (10 : ℕ) * (v.gcd w * M) ≤ w * M.
  Uses library Nat.mul_assoc, Nat.mul_le_mul_right.
  Lean, lines 74–75
  · have h2 : 10 * (v.gcd w * M) ≤ w * M := by rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right M h
  targets/erdos-402/nodes/variant-a5969ff3/Proof.lean, lines 74–75 at b48e57a81803 ↗

The proof in Lean (Proof.lean)

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

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-a5969ff3/Proof.lean, sha256 56e38fca3acf.

import Mathlib
import Nodes.«variant-a5969ff3».Context

/-! Graham's gcd conjecture (Erdős problem 402) for 10-element sets: with M the largest element,
if every b had gcd(M, b) > M/10 then every other element would be (j/k)M with j < k < 10, and a
colouring of those values into 8 classes, each a set of pairwise "good" values, shows the
9 other elements cannot all avoid a pair x, y with 10 * gcd(x, y) ≤ max(x, y). -/

theorem Opn.erdos_402_card_ten :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 10 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A h0 hcard
  -- the rational inequality is 10 * gcd a b ≤ a
  have red : ∀ a b : ℕ, 10 * a.gcd b ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
    intro a b h
    rw [hcard, le_div_iff₀ (by norm_num)]
    exact_mod_cast (by omega : a.gcd b * 10 ≤ a)
  have hne : A.Nonempty := Finset.card_pos.mp (by omega)
  obtain ⟨M, hMA, hMmax⟩ : ∃ M ∈ A, ∀ x ∈ A, x ≤ M :=
    ⟨A.max' hne, A.max'_mem hne, fun x hx => A.le_max' x hx⟩
  have hMpos : 0 < M := Nat.pos_of_ne_zero (by rintro rfl; exact h0 hMA)
  by_cases hsmall : ∃ x ∈ A, 10 * M.gcd x ≤ M
  · obtain ⟨x, hx, h⟩ := hsmall
    exact ⟨M, hMA, x, hx, red M x h⟩
  push Not at hsmall
  -- every other element x has 2520 * x = v * M for one of the 27 values v = 2520 * j / k
  have hval : ∀ x ∈ A.erase M, ∃ v ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), 2520 * x = v * M := by
    intro x hx
    obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero (by rintro rfl; exact h0 hxA)
    have hlt : x < M := lt_of_le_of_ne (hMmax x hxA) hxM
    have hbig : M < 10 * M.gcd x := hsmall x hxA
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left M x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right M x
    have hk10 : k < 10 := by
      by_contra hh
      have : M.gcd x * 10 ≤ M.gcd x * k := Nat.mul_le_mul_left _ (by omega)
      omega
    have hjk : j < k := by
      have : M.gcd x * j < M.gcd x * k := by omega
      exact Nat.lt_of_mul_lt_mul_left this
    have hj0 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · rw [h, Nat.mul_zero] at hj; omega
      · exact h
    refine ⟨2520 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega
  -- colour the 27 values with 8 colours, each colour class pairwise good
  have hcol : ∀ v ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) v < 8 := by decide
  have hgood : ∀ v ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), ∀ w ∈ ({280, 315, 360, 420, 504, 560, 630, 720, 840, 945, 1008, 1080, 1120, 1260, 1400, 1440, 1512, 1575, 1680, 1800, 1890, 1960, 2016, 2100, 2160, 2205, 2240} : Finset ℕ), v ≠ w → (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) v = (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) w →
      10 * v.gcd w ≤ v ∨ 10 * v.gcd w ≤ w := by decide
  have hmaps : ∀ x ∈ A.erase M, (fun a : ℕ => if a = 280 then 4 else if a = 315 then 6 else if a = 360 then 2 else if a = 420 then 5 else if a = 504 then 7 else if a = 560 then 6 else if a = 630 then 3 else if a = 720 then 5 else if a = 840 then 1 else if a = 945 then 2 else if a = 1008 then 4 else if a = 1080 then 3 else if a = 1120 then 3 else if a = 1260 then 0 else if a = 1400 then 0 else if a = 1440 then 4 else if a = 1512 then 5 else if a = 1575 then 5 else if a = 1680 then 2 else if a = 1800 then 1 else if a = 1890 then 4 else if a = 1960 then 5 else if a = 2016 then 1 else if a = 2100 then 3 else if a = 2160 then 0 else if a = 2205 then 1 else if a = 2240 then 7 else 0) (2520 * x / M) ∈ Finset.range 8 := by
    intro x hx
    obtain ⟨v, hv, hxv⟩ := hval x hx
    rw [Finset.mem_range, hxv, Nat.mul_div_cancel _ hMpos]
    exact hcol v hv
  have h9 : (A.erase M).card = 9 := by rw [Finset.card_erase_of_mem hMA, hcard]
  obtain ⟨x, hx, y, hy, hxy, hc⟩ :=
    Finset.exists_ne_map_eq_of_card_lt_of_maps_to (by rw [h9, Finset.card_range]; omega) hmaps
  obtain ⟨v, hv, hxv⟩ := hval x hx
  obtain ⟨w, hw, hyw⟩ := hval y hy
  rw [hxv, hyw, Nat.mul_div_cancel _ hMpos, Nat.mul_div_cancel _ hMpos] at hc
  have hvw : v ≠ w := by
    rintro rfl
    exact hxy (by omega)
  have hg : v.gcd w * M = 2520 * x.gcd y := by
    rw [← Nat.gcd_mul_right, ← hxv, ← hyw, Nat.gcd_mul_left]
  have hxA := (Finset.mem_erase.mp hx).2
  have hyA := (Finset.mem_erase.mp hy).2
  rcases hgood v hv w hw hvw hc with h | h
  · have h2 : 10 * (v.gcd w * M) ≤ v * M := by
      rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right M h
    exact ⟨x, hxA, y, hyA, red x y (by omega)⟩
  · have h2 : 10 * (v.gcd w * M) ≤ w * M := by
      rw [← Nat.mul_assoc]; exact Nat.mul_le_mul_right M h
    exact ⟨y, hyA, x, hxA, red y x (by rw [Nat.gcd_comm]; omega)⟩

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

/-! Graham's gcd conjecture (Erdős problem 402) for 10-element sets: with M the largest element,
if every b had gcd(M, b) > M/10 then every other element would be (j/k)M with j < k < 10, and a
colouring of those values into 8 classes, each a set of pairwise "good" values, shows the
9 other elements cannot all avoid a pair x, y with 10 * gcd(x, y) ≤ max(x, y). -/

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

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

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

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

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000244.json.

Submitter: t0929-5
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/000244.json, merge commit b48e57a81803.

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

import Mathlib

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 10 := ⟨Finset.Icc 1 10, 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-a5969ff3/Relation.lean, sha256 ee9b7ff9f3dd.

-- 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 = 10 → ∃ 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 = 10 is a hypothesis, so the divisor is non-zero wherever the conclusion is evaluated; the same division appears in the root statement.

How to read this page

How to read a statement’s page →