Graham's bound for size n from a colouring certificate

spec-fa8046e4 Opn.erdos_402_card_of_colouring

proved

Proposed by a contributor.

$\displaystyle \begin{aligned}&n \ge 2,\ L > 0,\ S \subset \mathbb{N}\ \text{finite},\ c : \mathbb{N} \to \mathbb{N},\\&\forall k < n,\ \forall j < k,\ j > 0:\ k \mid L j\ \wedge\ L j / k \in S,\qquad \forall a \in S:\ c(a) + 2 < n,\\&\forall a, b \in S,\ a \ne b,\ c(a) = c(b):\ n \cdot \gcd(a,b) \le a\ \vee\ n \cdot \gcd(a,b) \le b\\&\Longrightarrow\ \forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = n \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}\end{aligned}$

Given n ≥ 2, a positive L, a finite set S ⊂ ℕ and a colouring c such that every L·j/k with 0 < j < k < n is an integer lying in S, every colour c(a) of an element of S is below n − 2, and two distinct elements of S of the same colour a, b satisfy n·gcd(a, b) ≤ a or n·gcd(a, b) ≤ b: every set A of exactly n positive integers has a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. L·j/k is natural-number division, exact because k divides L·j; the last division is in ℚ.

unverified · history

Lean

theorem Opn.erdos_402_card_of_colouring :
    ∀ (n L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ), 2 ≤ n → 0 < L →
      (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, 0 < j → k ∣ L * j ∧ L * j / k ∈ S) →
      (∀ a ∈ S, c a + 2 < n) →
      (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) →
      ∀ A : Finset ℕ, 0 ∉ A → A.card = n → ∃ 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, 000288, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000288.json, merge commit 49badf930c2e.

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 19
```
  have hpos : 0 < A.card := by omega
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 19 at 49badf930c2e ↗
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 20
```
  have hne : A.Nonempty := Finset.card_pos.mp hpos
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 20 at 49badf930c2e ↗
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 21–24
```
  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/spec-fa8046e4/Proof.lean, lines 21–24 at 49badf930c2e ↗
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 25
```
  have hM : A.max' hne ∈ A := Finset.max'_mem A hne
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 25 at 49badf930c2e ↗
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 26
```
  have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 26 at 49badf930c2e ↗
s6 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro.
Lean, lines 28–29
```
  · obtain ⟨x, hx, h⟩ := hw
    exact ⟨_, hM, x, hx, key _ x (by rw [hcard]; exact h)⟩
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 28–29 at 49badf930c2e ↗
1. s6.s1 obtain ∃ x ∈ A, (A.max' hne).gcd x * n ≤ 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 * n ≤ A.max' hne.
  Lean, line 28
  · obtain ⟨x, hx, h⟩ := hw
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 28 at 49badf930c2e ↗
forms have ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne.
Uses library Finset.mem_erase, Exists.intro, Nat.mul_div_cancel_left, Nat.eq_of_mul_eq_mul_left.
Lean, lines 31–70
```
  have forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne := by
    intro x hx
    rw [Finset.mem_erase] at hx
    obtain ⟨hxM, hxA⟩ := hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))
    have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
    have hg := hw x hxA
    have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
    have hj1 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · rw [h, Nat.mul_zero] at hj
        omega
      · exact h
    have hjk : j < k := by
      have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
        rw [← hj, ← hk]
        exact hlt
      exact Nat.lt_of_mul_lt_mul_left h1
    have hkn : k < n := by
      have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
        rw [← hk]
        exact hg
      exact Nat.lt_of_mul_lt_mul_left h1
    have hkx : k * x = j * A.max' hne := by
      calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
        _ = j * ((A.max' hne).gcd x * k) := by ring
        _ = j * A.max' hne := by rw [← hk]
    have hkpos : 0 < k := by omega
    obtain ⟨hdvd, hmem⟩ := hS k (Finset.mem_range.2 hkn) j (Finset.mem_range.2 hjk) hj1
    obtain ⟨q, hq⟩ := hdvd
    refine ⟨L * j / k, hmem, ?_⟩
    rw [hq, Nat.mul_div_cancel_left q hkpos]
    apply Nat.eq_of_mul_eq_mul_left hkpos
    calc k * (L * x) = L * (k * x) := by ring
      _ = L * (j * A.max' hne) := by rw [hkx]
      _ = (L * j) * A.max' hne := by ring
      _ = (k * q) * A.max' hne := by rw [hq]
      _ = k * (q * A.max' hne) := by ring
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 31–70 at 49badf930c2e ↗
1. forms.s1 obtain x ≠ A.max' hne ∧ x ∈ A
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hxM : x ≠ A.max' hne, hxA : x ∈ A.
  Lean, line 34
  obtain ⟨hxM, hxA⟩ := hx
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 34 at 49badf930c2e ↗
2. forms.hxpos have (0 : ℕ) < x
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hxpos : (0 : ℕ) < x.
  Uses library Nat.pos_of_ne_zero.
  Lean, line 35
  have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 35 at 49badf930c2e ↗
3. forms.hlt have x < A.max' hne
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hlt : x < A.max' hne.
  Uses library lt_of_le_of_ne, Finset.le_max'.
  Lean, line 36
  have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 36 at 49badf930c2e ↗
4. forms.hg have A.max' hne < (A.max' hne).gcd x * n
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hg : A.max' hne < (A.max' hne).gcd x * n.
  Lean, line 37
  have hg := hw x hxA
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 37 at 49badf930c2e ↗
5. forms.hgpos have (0 : ℕ) < (A.max' hne).gcd x
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hgpos : (0 : ℕ) < (A.max' hne).gcd x.
  Uses library Nat.gcd_pos_of_pos_right.
  Lean, line 38
  have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 38 at 49badf930c2e ↗
6. forms.s6 obtain (A.max' hne).gcd x ∣ A.max' hne
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with k : ℕ, hk : A.max' hne = (A.max' hne).gcd x * k.
  Uses library Nat.gcd_dvd_left.
  Lean, line 39
  obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 39 at 49badf930c2e ↗
7. forms.s7 obtain (A.max' hne).gcd x ∣ x
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with j : ℕ, hj : x = (A.max' hne).gcd x * j.
  Uses library Nat.gcd_dvd_right.
  Lean, line 40
  obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 40 at 49badf930c2e ↗
8. forms.hj1 have (0 : ℕ) < j
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hj1 : (0 : ℕ) < j.
  Uses library Nat.eq_zero_or_pos.
  Lean, lines 41–45
  have hj1 : 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/spec-fa8046e4/Proof.lean, lines 41–45 at 49badf930c2e ↗
  forms.hj1.s1 case
  Leaves (0 : ℕ) < j.
  Uses library Nat.mul_zero.
  Lean, lines 43–44
  · rw [h, Nat.mul_zero] at hj omega
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 43–44 at 49badf930c2e ↗
  forms.hj1.s2 case
  Leaves (0 : ℕ) < j.
  Lean, line 45
  · exact h
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 45 at 49badf930c2e ↗
9. forms.hjk have j < k
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hjk : j < k.
  Uses library Nat.lt_of_mul_lt_mul_left.
  Lean, lines 46–50
  have hjk : j < k := by have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by rw [← hj, ← hk] exact hlt exact Nat.lt_of_mul_lt_mul_left h1
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 46–50 at 49badf930c2e ↗
  forms.hjk.h1 have (A.max' hne).gcd x * j < (A.max' hne).gcd x * k
  Leaves j < k, with h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k.
  Lean, lines 47–49
  have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by rw [← hj, ← hk] exact hlt
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 47–49 at 49badf930c2e ↗
10. forms.hkn have k < n
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hkn : k < n.
  Uses library Nat.lt_of_mul_lt_mul_left.
  Lean, lines 51–55
  have hkn : k < n := by have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by rw [← hk] exact hg exact Nat.lt_of_mul_lt_mul_left h1
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 51–55 at 49badf930c2e ↗
  forms.hkn.h1 have (A.max' hne).gcd x * k < (A.max' hne).gcd x * n
  Leaves k < n, with h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n.
  Lean, lines 52–54
  have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by rw [← hk] exact hg
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 52–54 at 49badf930c2e ↗
11. forms.hkx have k * x = j * A.max' hne
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hkx : k * x = j * A.max' hne.
  Lean, lines 56–59
  have hkx : k * x = j * A.max' hne := by calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj] _ = j * ((A.max' hne).gcd x * k) := by ring _ = j * A.max' hne := by rw [← hk]
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 56–59 at 49badf930c2e ↗
  forms.hkx.s1 calc k * x = k * ((A.max' hne).gcd x * j)
  Closes the goal.
  Lean, line 57
  calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 57 at 49badf930c2e ↗
  forms.hkx.s2 calc routine: ring
  Closes the goal.
  Lean, line 58
  _ = j * ((A.max' hne).gcd x * k) := by ring
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 58 at 49badf930c2e ↗
  forms.hkx.s3 calc
  Closes the goal.
  Lean, line 59
  _ = j * A.max' hne := by rw [← hk]
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 59 at 49badf930c2e ↗
12. forms.hkpos have (0 : ℕ) < k routine: omega
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hkpos : (0 : ℕ) < k.
  Lean, line 60
  have hkpos : 0 < k := by omega
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 60 at 49badf930c2e ↗
13. forms.s13 obtain k ∣ L * j ∧ L * j / k ∈ S
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with hdvd : k ∣ L * j, hmem : L * j / k ∈ S.
  Uses library Finset.mem_range.
  Lean, line 61
  obtain ⟨hdvd, hmem⟩ := hS k (Finset.mem_range.2 hkn) j (Finset.mem_range.2 hjk) hj1
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 61 at 49badf930c2e ↗
14. forms.s14 obtain k ∣ L * j
  Leaves ∃ a ∈ S, L * x = a * A.max' hne, with q : ℕ, hq : L * j = k * q.
  Lean, line 62
  obtain ⟨q, hq⟩ := hdvd
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 62 at 49badf930c2e ↗
15. forms.s15 calc k * (L * x) = L * (k * x) routine: ring
  Closes the goal.
  Lean, line 66
  calc k * (L * x) = L * (k * x) := by ring
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 66 at 49badf930c2e ↗
16. forms.s16 calc
  Closes the goal.
  Lean, line 67
  _ = L * (j * A.max' hne) := by rw [hkx]
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 67 at 49badf930c2e ↗
17. forms.s17 calc routine: ring
  Closes the goal.
  Lean, line 68
  _ = (L * j) * A.max' hne := by ring
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 68 at 49badf930c2e ↗
18. forms.s18 calc
  Closes the goal.
  Lean, line 69
  _ = (k * q) * A.max' hne := by rw [hq]
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 69 at 49badf930c2e ↗
19. forms.s19 calc routine: ring
  Closes the goal.
  Lean, line 70
  _ = k * (q * A.max' hne) := by ring
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 70 at 49badf930c2e ↗
hmaps have ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - (2 : ℕ))
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - (2 : ℕ)).
Uses library Finset.range, Finset.mem_range, Nat.mul_div_cancel.
Lean, lines 71–76
```
  have hmaps : ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - 2) := by
    intro x hx
    obtain ⟨a, ha, hax⟩ := forms x hx
    rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
    have := hc a ha
    omega
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 71–76 at 49badf930c2e ↗
1. hmaps.s1 obtain ∃ a ∈ S, L * x = a * A.max' hne
  Leaves c (L * x / A.max' hne) ∈ Finset.range (n - (2 : ℕ)), with a : ℕ, ha : a ∈ S, hax : L * x = a * A.max' hne.
  Lean, line 73
  obtain ⟨a, ha, hax⟩ := forms x hx
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 73 at 49badf930c2e ↗
2. hmaps.this have c a + (2 : ℕ) < n
  Leaves c a < n - (2 : ℕ), with this : c a + (2 : ℕ) < n.
  Lean, line 75
  have := hc a ha
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 75 at 49badf930c2e ↗
hcardE have (A.erase (A.max' hne)).card = n - (1 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcardE : (A.erase (A.max' hne)).card = n - (1 : ℕ).
Uses library Finset.card_erase_of_mem.
Lean, lines 77–78
```
  have hcardE : (A.erase (A.max' hne)).card = n - 1 := by
    rw [Finset.card_erase_of_mem hM, hcard]
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 77–78 at 49badf930c2e ↗
s10 obtain ∃ x ∈ A.erase (A.max' hne), ∃ y ∈ A.erase (A.max' hne), x ≠ y ∧ c (L * x / A.max' hne) = c (L * y / A.max' hne)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A.erase (A.max' hne), y : ℕ, hy : y ∈ A.erase (A.max' hne), hxy : x ≠ y, hcol : c (L * x / A.max' hne) = c (L * y / A.max' hne).
Uses library Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.card_range.
Lean, lines 79–81
```
  obtain ⟨x, hx, y, hy, hxy, hcol⟩ :=
    Finset.exists_ne_map_eq_of_card_lt_of_maps_to
      (by rw [hcardE, Finset.card_range]; omega) hmaps
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 79–81 at 49badf930c2e ↗
s11 obtain ∃ a ∈ S, L * x = a * A.max' hne
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with a : ℕ, ha : a ∈ S, hax : L * x = a * A.max' hne.
Lean, line 82
```
  obtain ⟨a, ha, hax⟩ := forms x hx
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 82 at 49badf930c2e ↗
s12 obtain ∃ a ∈ S, L * y = a * A.max' hne
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with b : ℕ, hb : b ∈ S, hby : L * y = b * A.max' hne.
Lean, line 83
```
  obtain ⟨b, hb, hby⟩ := forms y hy
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 83 at 49badf930c2e ↗
hab have a ≠ b
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hab : a ≠ b.
Uses library Nat.eq_of_mul_eq_mul_left.
Lean, lines 85–89
```
  have hab : a ≠ b := by
    intro h
    apply hxy
    apply Nat.eq_of_mul_eq_mul_left hL
    rw [hax, hby, h]
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 85–89 at 49badf930c2e ↗
hgcd have a.gcd b * A.max' hne = L * x.gcd y
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgcd : a.gcd b * A.max' hne = L * x.gcd y.
Uses library Nat.gcd_mul_right.
Lean, lines 90–93
```
  have hgcd : a.gcd b * A.max' hne = L * x.gcd y := by
    have h1 : Nat.gcd (L * x) (L * y) = L * x.gcd y := Nat.gcd_mul_left L x y
    rw [hax, hby, Nat.gcd_mul_right] at h1
    exact h1
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 90–93 at 49badf930c2e ↗
1. hgcd.h1 have (L * x).gcd (L * y) = L * x.gcd y
  Leaves a.gcd b * A.max' hne = L * x.gcd y, with h1 : (L * x).gcd (L * y) = L * x.gcd y.
  Uses library Nat.gcd, Nat.gcd_mul_left.
  Lean, line 91
  have h1 : Nat.gcd (L * x) (L * y) = L * x.gcd y := Nat.gcd_mul_left L x y
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 91 at 49badf930c2e ↗
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 94
```
  have hxA := (Finset.mem_erase.mp hx).2
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 94 at 49badf930c2e ↗
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 95
```
  have hyA := (Finset.mem_erase.mp hy).2
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 95 at 49badf930c2e ↗
s17 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro, Nat.le_of_mul_le_mul_left.
Lean, lines 97–103
```
  · refine ⟨x, hxA, y, hyA, key x y ?_⟩
    rw [hcard]
    have h2 : L * (x.gcd y * n) ≤ L * x := by
      calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
        _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
        _ = L * x := hax.symm
    exact Nat.le_of_mul_le_mul_left h2 hL
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 97–103 at 49badf930c2e ↗
1. s17.h2 have L * (x.gcd y * n) ≤ L * x
  Leaves x.gcd y * n ≤ x, with h2 : L * (x.gcd y * n) ≤ L * x.
  Lean, lines 99–102
  have h2 : L * (x.gcd y * n) ≤ L * x := by calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring) _ = L * x := hax.symm
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 99–102 at 49badf930c2e ↗
  s17.h2.s1 calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne)
  Closes the goal.
  Lean, line 100
  calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 100 at 49badf930c2e ↗
  s17.h2.s2 calc n * (a.gcd b * A.max' hne) ≤ a * A.max' hne
  Closes the goal.
  Uses library Nat.mul_le_mul_right.
  Lean, line 101
  _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 101 at 49badf930c2e ↗
  s17.h2.s3 calc a * A.max' hne = L * x
  Closes the goal.
  Lean, line 102
  _ = L * x := hax.symm
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 102 at 49badf930c2e ↗
s18 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro, Nat.gcd_comm, Nat.le_of_mul_le_mul_left.
Lean, lines 104–110
```
  · refine ⟨y, hyA, x, hxA, key y x ?_⟩
    rw [hcard, Nat.gcd_comm]
    have h2 : L * (x.gcd y * n) ≤ L * y := by
      calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
        _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
        _ = L * y := hby.symm
    exact Nat.le_of_mul_le_mul_left h2 hL
```
targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 104–110 at 49badf930c2e ↗
1. s18.h2 have L * (x.gcd y * n) ≤ L * y
  Leaves x.gcd y * n ≤ y, with h2 : L * (x.gcd y * n) ≤ L * y.
  Lean, lines 106–109
  have h2 : L * (x.gcd y * n) ≤ L * y := by calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring) _ = L * y := hby.symm
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, lines 106–109 at 49badf930c2e ↗
  s18.h2.s1 calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne)
  Closes the goal.
  Lean, line 107
  calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 107 at 49badf930c2e ↗
  s18.h2.s2 calc n * (a.gcd b * A.max' hne) ≤ b * A.max' hne
  Closes the goal.
  Uses library Nat.mul_le_mul_right.
  Lean, line 108
  _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 108 at 49badf930c2e ↗
  s18.h2.s3 calc b * A.max' hne = L * y
  Closes the goal.
  Lean, line 109
  _ = L * y := hby.symm
  targets/erdos-402/nodes/spec-fa8046e4/Proof.lean, line 109 at 49badf930c2e ↗

The proof in Lean (Proof.lean)

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

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/spec-fa8046e4/Proof.lean, sha256 546f65141014.

import Mathlib
import Nodes.«spec-fa8046e4».Context

/-! A reduction of every fixed-size case of Erdős problem 402 (Graham's gcd problem) to a finite
certificate. With M the largest element of A, if gcd(M, x) ≤ M/n for some x the pair (M, x)
answers; otherwise every other element x is (j/k)·M with 1 ≤ j < k < n, so L·x = a·M for the
value a = L·j/k in S. The n − 1 other elements land on distinct values of S, and a colouring c
of S with n − 2 colours whose equal-coloured pairs a ≠ b all have n·gcd(a, b) ≤ max(a, b) gives,
by pigeonhole, two elements x, y with n·gcd(x, y) ≤ x or ≤ y, because gcd(a, b)·M = L·gcd(x, y).
A card-n variant then needs only L, S and c, and three decidable checks. -/

theorem Opn.erdos_402_card_of_colouring :
    ∀ (n L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ), 2 ≤ n → 0 < L →
      (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, 0 < j → k ∣ L * j ∧ L * j / k ∈ S) →
      (∀ a ∈ S, c a + 2 < n) →
      (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) →
      ∀ A : Finset ℕ, 0 ∉ A → A.card = n → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro n L S c hn hL hS hc hgood A hA hcard
  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))
  by_cases hw : ∃ x ∈ A, (A.max' hne).gcd x * n ≤ A.max' hne
  · obtain ⟨x, hx, h⟩ := hw
    exact ⟨_, hM, x, hx, key _ x (by rw [hcard]; exact h)⟩
  push_neg at hw
  have forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ S, L * x = a * A.max' hne := by
    intro x hx
    rw [Finset.mem_erase] at hx
    obtain ⟨hxM, hxA⟩ := hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))
    have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
    have hg := hw x hxA
    have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
    obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
    have hj1 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · rw [h, Nat.mul_zero] at hj
        omega
      · exact h
    have hjk : j < k := by
      have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
        rw [← hj, ← hk]
        exact hlt
      exact Nat.lt_of_mul_lt_mul_left h1
    have hkn : k < n := by
      have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
        rw [← hk]
        exact hg
      exact Nat.lt_of_mul_lt_mul_left h1
    have hkx : k * x = j * A.max' hne := by
      calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
        _ = j * ((A.max' hne).gcd x * k) := by ring
        _ = j * A.max' hne := by rw [← hk]
    have hkpos : 0 < k := by omega
    obtain ⟨hdvd, hmem⟩ := hS k (Finset.mem_range.2 hkn) j (Finset.mem_range.2 hjk) hj1
    obtain ⟨q, hq⟩ := hdvd
    refine ⟨L * j / k, hmem, ?_⟩
    rw [hq, Nat.mul_div_cancel_left q hkpos]
    apply Nat.eq_of_mul_eq_mul_left hkpos
    calc k * (L * x) = L * (k * x) := by ring
      _ = L * (j * A.max' hne) := by rw [hkx]
      _ = (L * j) * A.max' hne := by ring
      _ = (k * q) * A.max' hne := by rw [hq]
      _ = k * (q * A.max' hne) := by ring
  have hmaps : ∀ x ∈ A.erase (A.max' hne), c (L * x / A.max' hne) ∈ Finset.range (n - 2) := by
    intro x hx
    obtain ⟨a, ha, hax⟩ := forms x hx
    rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
    have := hc a ha
    omega
  have hcardE : (A.erase (A.max' hne)).card = n - 1 := by
    rw [Finset.card_erase_of_mem hM, hcard]
  obtain ⟨x, hx, y, hy, hxy, hcol⟩ :=
    Finset.exists_ne_map_eq_of_card_lt_of_maps_to
      (by rw [hcardE, Finset.card_range]; omega) hmaps
  obtain ⟨a, ha, hax⟩ := forms x hx
  obtain ⟨b, hb, hby⟩ := forms y hy
  rw [hax, hby, Nat.mul_div_cancel _ hMpos, Nat.mul_div_cancel _ hMpos] at hcol
  have hab : a ≠ b := by
    intro h
    apply hxy
    apply Nat.eq_of_mul_eq_mul_left hL
    rw [hax, hby, h]
  have hgcd : a.gcd b * A.max' hne = L * x.gcd y := by
    have h1 : Nat.gcd (L * x) (L * y) = L * x.gcd y := Nat.gcd_mul_left L x y
    rw [hax, hby, Nat.gcd_mul_right] at h1
    exact h1
  have hxA := (Finset.mem_erase.mp hx).2
  have hyA := (Finset.mem_erase.mp hy).2
  rcases hgood a ha b hb hab hcol with h | h
  · refine ⟨x, hxA, y, hyA, key x y ?_⟩
    rw [hcard]
    have h2 : L * (x.gcd y * n) ≤ L * x := by
      calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
        _ ≤ a * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
        _ = L * x := hax.symm
    exact Nat.le_of_mul_le_mul_left h2 hL
  · refine ⟨y, hyA, x, hxA, key y x ?_⟩
    rw [hcard, Nat.gcd_comm]
    have h2 : L * (x.gcd y * n) ≤ L * y := by
      calc L * (x.gcd y * n) = n * (a.gcd b * A.max' hne) := by rw [hgcd]; ring
        _ ≤ b * A.max' hne := Nat.mul_le_mul_right _ h |>.trans_eq' (by ring)
        _ = L * y := hby.symm
    exact Nat.le_of_mul_le_mul_left h2 hL

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.«spec-fa8046e4».Context

/-! A reduction of every fixed-size case of Erdős problem 402 (Graham's gcd problem) to a finite
certificate. With M the largest element of A, if gcd(M, x) ≤ M/n for some x the pair (M, x)
answers; otherwise every other element x is (j/k)·M with 1 ≤ j < k < n, so L·x = a·M for the
value a = L·j/k in S. The n − 1 other elements land on distinct values of S, and a colouring c
of S with n − 2 colours whose equal-coloured pairs a ≠ b all have n·gcd(a, b) ≤ max(a, b) gives,
by pigeonhole, two elements x, y with n·gcd(x, y) ≤ x or ≤ y, because gcd(a, b)·M = L·gcd(x, y).
A card-n variant then needs only L, S and c, and three decidable checks. -/

theorem Opn.erdos_402_card_of_colouring :
    ∀ (n L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ), 2 ≤ n → 0 < L →
      (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, 0 < j → k ∣ L * j ∧ L * j / k ∈ S) →
      (∀ a ∈ S, c a + 2 < n) →
      (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) →
      ∀ A : Finset ℕ, 0 ∉ A → A.card = n → ∃ 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

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

Rendered from targets/erdos-402/nodes/spec-fa8046e4/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000288.json, merge commit 49badf930c2e.

Verdict pass, from attestations/000288.json.

Submitter: t0929-6
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/000288.json, merge commit 49badf930c2e.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/spec-fa8046e4/Witness.lean, sha256 719986e743e4.

import Mathlib

/-! The certificate for three-element sets: the only fraction (j/k)·M with 1 ≤ j < k < 3 is M/2,
so L = 2, S = {1} and one colour. -/

theorem witness : ∃ (n : ℕ) (L : ℕ) (S : Finset ℕ) (c : ℕ → ℕ) (A : Finset ℕ),
    (2 : ℕ) ≤ n ∧
      (0 : ℕ) < L ∧
        (∀ k ∈ Finset.range n, ∀ j ∈ Finset.range k, (0 : ℕ) < j → k ∣ L * j ∧ L * j / k ∈ S) ∧
          (∀ a ∈ S, c a + (2 : ℕ) < n) ∧
            (∀ a ∈ S, ∀ b ∈ S, a ≠ b → c a = c b → n * a.gcd b ≤ a ∨ n * a.gcd b ≤ b) ∧
              (0 : ℕ) ∉ A ∧ A.card = n :=
  ⟨3, 2, {1}, fun _ => 0, {1, 2, 3}, by decide, by decide, by decide, by decide, by decide,
    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 →

Acknowledged findings (3)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at L * j / k

k ranges over 1 ≤ j < k, so k is positive, and the same hypothesis asserts k ∣ L * j, so the division is exact.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a div-zero finding at ↑a / ↑A.card

This is the conclusion of Erdős 402 as the root states it; A.card = n ≥ 2 makes the rational division by a positive number.

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a off-by-one-range finding at 2 ≤ n

The bound is intended: it excludes n = 0, where the empty set would make the statement false, and n = 1, which has no colour class; every case of interest has n ≥ 2.

How to read this page

How to read a statement’s page →