Open Proof Network

Problems / erdos-402 / variant-892f5809

Graham's bound for |A| = 9

variant-892f5809

proved

A partial route to the problem.

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

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

The proof step by step (outline)

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

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. toQ have ∀ (a b : ℕ), (9 : ℕ) * a.gcd b ≤ a → (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with toQ : ∀ (a b : ℕ), (9 : ℕ) * a.gcd b ≤ 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 12–16
      have toQ : ∀ a b : ℕ, 9 * a.gcd b ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
    intro a b hab
    have h9 : ((A.card : ℕ) : ℚ) = 9 := by rw [hcard]; norm_num
    rw [h9, le_div_iff₀ (by norm_num : (0 : ℚ) < 9)]
    exact_mod_cast (by omega : a.gcd b * 9 ≤ a)

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 12–16 at bc7b614c54a9 ↗

    1. toQ.h9 have (↑A.card : ℚ) = (9 : ℚ)

      Leaves (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with h9 : (↑A.card : ℚ) = (9 : ℚ).

      Lean, line 14
          have h9 : ((A.card : ℕ) : ℚ) = 9 := by rw [hcard]; norm_num

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 14 at bc7b614c54a9 ↗

  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 17
      have hne : A.Nonempty := Finset.card_pos.mp (by omega)

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 17 at bc7b614c54a9 ↗

  3. hMA have A.max' hne ∈ A

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

    Uses library Finset.max'_mem.

    Lean, line 18
      have hMA : A.max' hne ∈ A := Finset.max'_mem A hne

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 18 at bc7b614c54a9 ↗

  4. 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 19
      have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero fun h => h0 (h ▸ hMA)

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 19 at bc7b614c54a9 ↗

  5. s5 case

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

    Uses library Exists.intro Existential introduction. .

    Lean, lines 21–22
      · obtain ⟨x, hxA, hx⟩ := hdirect
    exact ⟨A.max' hne, hMA, x, hxA, toQ _ x hx⟩

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 21–22 at bc7b614c54a9 ↗

    1. s5.s1 obtain ∃ x ∈ A, (9 : ℕ) * (A.max' hne).gcd x ≤ A.max' hne

      Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hxA : x ∈ A, hx : (9 : ℕ) * (A.max' hne).gcd x ≤ A.max' hne.

      Lean, line 21
        · obtain ⟨x, hxA, hx⟩ := hdirect

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 21 at bc7b614c54a9 ↗

  6. hval have ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hval : ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne.

    Uses library Exists.intro Existential introduction. .

    Lean, lines 25–50
      have hval : ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ [105, 120, 140, 168, 210, 240, 280, 315, 336, 360,
      420, 480, 504, 525, 560, 600, 630, 672, 700, 720, 735], 840 * x = c * A.max' hne := by
    intro x hx
    obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero fun h => h0 (h ▸ hxA)
    have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
    have hbig : A.max' hne < 9 * (A.max' hne).gcd x := hdirect x hxA
    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
    have hk9 : k < 9 := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    have hjk : j < k := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    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 ⟨840 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 25–50 at bc7b614c54a9 ↗

    1. hval.s1 obtain x ≠ A.max' hne ∧ x ∈ A

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hxM : x ≠ A.max' hne, hxA : x ∈ A.

      Uses library Finset.mem_erase.

      Lean, line 28
          obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 28 at bc7b614c54a9 ↗

    2. hval.hxpos have (0 : ℕ) < x

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hxpos : (0 : ℕ) < x.

      Uses library Nat.pos_of_ne_zero.

      Lean, line 29
          have hxpos : 0 < x := Nat.pos_of_ne_zero fun h => h0 (h ▸ hxA)

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 29 at bc7b614c54a9 ↗

    3. hval.hxlt have x < A.max' hne

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hxlt : x < A.max' hne.

      Uses library lt_of_le_of_ne, Finset.le_max'.

      Lean, line 30
          have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 30 at bc7b614c54a9 ↗

    4. hval.hbig have A.max' hne < (9 : ℕ) * (A.max' hne).gcd x

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hbig : A.max' hne < (9 : ℕ) * (A.max' hne).gcd x.

      Lean, line 31
          have hbig : A.max' hne < 9 * (A.max' hne).gcd x := hdirect x hxA

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 31 at bc7b614c54a9 ↗

    5. hval.s5 obtain (A.max' hne).gcd x ∣ A.max' hne

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with k : ℕ, hk : A.max' hne = (A.max' hne).gcd x * k.

      Uses library Nat.gcd_dvd_left.

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

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 32 at bc7b614c54a9 ↗

    6. hval.s6 obtain (A.max' hne).gcd x ∣ x

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with j : ℕ, hj : x = (A.max' hne).gcd x * j.

      Uses library Nat.gcd_dvd_right.

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

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 33 at bc7b614c54a9 ↗

    7. hval.hgpos have (0 : ℕ) < (A.max' hne).gcd x

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hgpos : (0 : ℕ) < (A.max' hne).gcd x.

      Uses library Nat.gcd_pos_of_pos_right.

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

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 34 at bc7b614c54a9 ↗

    8. hval.hk9 have k < (9 : ℕ)

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hk9 : k < (9 : ℕ).

      Lean, lines 35–38
          have hk9 : k < 9 := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 35–38 at bc7b614c54a9 ↗

      1. hval.hk9.this have (A.max' hne).gcd x * (9 : ℕ) ≤ (A.max' hne).gcd x * k

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

        Uses library Nat.mul_le_mul_left, not_lt.

        Lean, line 37
              have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)

        targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 37 at bc7b614c54a9 ↗

    9. hval.hjk have j < k

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hjk : j < k.

      Lean, lines 39–42
          have hjk : j < k := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 39–42 at bc7b614c54a9 ↗

      1. hval.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, not_lt.

        Lean, line 41
              have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)

        targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 41 at bc7b614c54a9 ↗

    10. hval.hj0 have (0 : ℕ) < j

      Leaves ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne, with hj0 : (0 : ℕ) < j.

      Uses library Nat.eq_zero_or_pos.

      Lean, lines 43–47
          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-892f5809/Proof.lean, lines 43–47 at bc7b614c54a9 ↗

      1. hval.hj0.s1 case

        Leaves (0 : ℕ) < j.

        Uses library Nat.mul_zero.

        Lean, lines 45–46
              · rw [h, Nat.mul_zero] at hj
        omega

        targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 45–46 at bc7b614c54a9 ↗

      2. hval.hj0.s2 case

        Leaves (0 : ℕ) < j.

        Lean, line 47
              · exact h

        targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 47 at bc7b614c54a9 ↗

    11. hval.s11 case

      Leaves (840 : ℕ) * j / k ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)].

      Lean, line 49
          · interval_cases k <;> interval_cases j <;> decide

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 49 at bc7b614c54a9 ↗

    12. hval.s12 case

      Leaves (840 : ℕ) * x = (840 : ℕ) * j / k * A.max' hne.

      Lean, line 50
          · interval_cases k <;> interval_cases j <;> omega

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 50 at bc7b614c54a9 ↗

  7. s7 obtain ∃ (cls : ℕ → List ℕ), cls = fun (i : ℕ) => [[(420 : ℕ), (600 : ℕ)], [(210 : ℕ), (360 : ℕ), (672 : ℕ), (700 : ℕ)], [(120 : ℕ), (560 : ℕ), (630 : ℕ)], [(105 : ℕ), (240 : ℕ), (504 : ℕ)], [(280 : ℕ), (315 : ℕ), (480 : ℕ)], [(168 : ℕ), (525 : ℕ), (720 : ℕ)], [(140 : ℕ), (336 : ℕ), (735 : ℕ)]].getD i []

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with cls : ℕ → List ℕ, hcls : cls = fun (i : ℕ) => [[(420 : ℕ), (600 : ℕ)], [(210 : ℕ), (360 : ℕ), (672 : ℕ), (700 : ℕ)], [(120 : ℕ), (560 : ℕ), (630 : ℕ)], [(105 : ℕ), (240 : ℕ), (504 : ℕ)], [(280 : ℕ), (315 : ℕ), (480 : ℕ)], [(168 : ℕ), (525 : ℕ), (720 : ℕ)], [(140 : ℕ), (336 : ℕ), (735 : ℕ)]].getD i [].

    Uses library List Linked lists: ordered lists, in which each element has a reference to the next element. , Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 52–54
      obtain ⟨cls, hcls⟩ : ∃ cls : ℕ → List ℕ, cls = fun i => [[420, 600], [210, 360, 672, 700],
      [120, 560, 630], [105, 240, 504], [280, 315, 480], [168, 525, 720], [140, 336, 735]].getD i [] :=
    ⟨_, rfl⟩

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 52–54 at bc7b614c54a9 ↗

  8. s8 obtain ∃ (col : ℕ → ℕ), col = fun (c : ℕ) => List.findIdx (fun (C : List ℕ) => C.contains c) [[(420 : ℕ), (600 : ℕ)], [(210 : ℕ), (360 : ℕ), (672 : ℕ), (700 : ℕ)], [(120 : ℕ), (560 : ℕ), (630 : ℕ)], [(105 : ℕ), (240 : ℕ), (504 : ℕ)], [(280 : ℕ), (315 : ℕ), (480 : ℕ)], [(168 : ℕ), (525 : ℕ), (720 : ℕ)], [(140 : ℕ), (336 : ℕ), (735 : ℕ)]]

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with col : ℕ → ℕ, hcol : col = fun (c : ℕ) => List.findIdx (fun (C : List ℕ) => C.contains c) [[(420 : ℕ), (600 : ℕ)], [(210 : ℕ), (360 : ℕ), (672 : ℕ), (700 : ℕ)], [(120 : ℕ), (560 : ℕ), (630 : ℕ)], [(105 : ℕ), (240 : ℕ), (504 : ℕ)], [(280 : ℕ), (315 : ℕ), (480 : ℕ)], [(168 : ℕ), (525 : ℕ), (720 : ℕ)], [(140 : ℕ), (336 : ℕ), (735 : ℕ)]].

    Uses library Exists.intro Existential introduction. , rfl rfl : a = a is the unique constructor of the equality type. .

    Lean, lines 55–57
      obtain ⟨col, hcol⟩ : ∃ col : ℕ → ℕ, col = fun c => [[420, 600], [210, 360, 672, 700],
      [120, 560, 630], [105, 240, 504], [280, 315, 480], [168, 525, 720], [140, 336, 735]].findIdx
      (fun C => C.contains c) := ⟨_, rfl⟩

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 55–57 at bc7b614c54a9 ↗

  9. hcover have ∀ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], col c < (7 : ℕ) ∧ c ∈ cls (col c)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcover : ∀ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], col c < (7 : ℕ) ∧ c ∈ cls (col c).

    Uses library List Linked lists: ordered lists, in which each element has a reference to the next element. .

    Lean, lines 58–61
      have hcover : ∀ c ∈ ([105, 120, 140, 168, 210, 240, 280, 315, 336, 360, 420, 480, 504, 525, 560,
      600, 630, 672, 700, 720, 735] : List ℕ), col c < 7 ∧ c ∈ cls (col c) := by
    subst hcol hcls
    decide

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 58–61 at bc7b614c54a9 ↗

  10. hgood have ∀ i < (7 : ℕ), ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ (9 : ℕ) * c.gcd d ≤ c ∨ (9 : ℕ) * c.gcd d ≤ d

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgood : ∀ i < (7 : ℕ), ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ (9 : ℕ) * c.gcd d ≤ c ∨ (9 : ℕ) * c.gcd d ≤ d.

    Lean, lines 62–64
      have hgood : ∀ i < 7, ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ 9 * c.gcd d ≤ c ∨ 9 * c.gcd d ≤ d := by
    subst hcls
    decide

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 62–64 at bc7b614c54a9 ↗

  11. hmaps have ∀ x ∈ A.erase (A.max' hne), col ((840 : ℕ) * x / A.max' hne) ∈ Finset.range (7 : ℕ)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase (A.max' hne), col ((840 : ℕ) * x / A.max' hne) ∈ Finset.range (7 : ℕ).

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.mem_range, Nat.mul_div_cancel.

    Lean, lines 66–70
      have hmaps : ∀ x ∈ A.erase (A.max' hne), col (840 * x / A.max' hne) ∈ Finset.range 7 := by
    intro x hx
    obtain ⟨c, hc, hxc⟩ := hval x hx
    rw [Finset.mem_range, hxc, Nat.mul_div_cancel _ hMpos]
    exact (hcover c hc).1

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 66–70 at bc7b614c54a9 ↗

    1. hmaps.s1 obtain ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne

      Leaves col ((840 : ℕ) * x / A.max' hne) ∈ Finset.range (7 : ℕ), with c : ℕ, hc : c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], hxc : (840 : ℕ) * x = c * A.max' hne.

      Lean, line 68
          obtain ⟨c, hc, hxc⟩ := hval x hx

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 68 at bc7b614c54a9 ↗

  12. hcard8 have (Finset.range (7 : ℕ)).card < (A.erase (A.max' hne)).card

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcard8 : (Finset.range (7 : ℕ)).card < (A.erase (A.max' hne)).card.

    Uses library Finset.range range n is the set of natural numbers less than n. , Finset.card_erase_of_mem $\#(s \setminus \{a\}) = \#s - 1$ if $a \in s$. , Finset.card_range.

    Lean, lines 71–73
      have hcard8 : (Finset.range 7).card < (A.erase (A.max' hne)).card := by
    rw [Finset.card_erase_of_mem hMA, hcard, Finset.card_range]
    norm_num

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 71–73 at bc7b614c54a9 ↗

  13. s13 obtain ∃ x ∈ A.erase (A.max' hne), ∃ y ∈ A.erase (A.max' hne), x ≠ y ∧ col ((840 : ℕ) * x / A.max' hne) = col ((840 : ℕ) * 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, hxycol : col ((840 : ℕ) * x / A.max' hne) = col ((840 : ℕ) * y / A.max' hne).

    Uses library Finset.exists_ne_map_eq_of_card_lt_of_maps_to If there are more pigeons than pigeonholes, then there are two pigeons in the same pigeonhole. .

    Lean, line 74
      obtain ⟨x, hx, y, hy, hxy, hxycol⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard8 hmaps

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 74 at bc7b614c54a9 ↗

  14. s14 obtain ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * x = c * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with c : ℕ, hc : c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], hxc : (840 : ℕ) * x = c * A.max' hne.

    Lean, line 75
      obtain ⟨c, hc, hxc⟩ := hval x hx

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 75 at bc7b614c54a9 ↗

  15. s15 obtain ∃ c ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], (840 : ℕ) * y = c * A.max' hne

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with d : ℕ, hd : d ∈ [(105 : ℕ), (120 : ℕ), (140 : ℕ), (168 : ℕ), (210 : ℕ), (240 : ℕ), (280 : ℕ), (315 : ℕ), (336 : ℕ), (360 : ℕ), (420 : ℕ), (480 : ℕ), (504 : ℕ), (525 : ℕ), (560 : ℕ), (600 : ℕ), (630 : ℕ), (672 : ℕ), (700 : ℕ), (720 : ℕ), (735 : ℕ)], hyd : (840 : ℕ) * y = d * A.max' hne.

    Lean, line 76
      obtain ⟨d, hd, hyd⟩ := hval y hy

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 76 at bc7b614c54a9 ↗

  16. hcd have c ≠ d

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcd : c ≠ d.

    Lean, lines 78–80
      have hcd : c ≠ d := by
    rintro rfl
    exact hxy (by omega)

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 78–80 at bc7b614c54a9 ↗

  17. hcmem have c ∈ cls (col c)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcmem : c ∈ cls (col c).

    Lean, line 81
      have hcmem := (hcover c hc).2

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 81 at bc7b614c54a9 ↗

  18. hdmem have d ∈ cls (col d)

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hdmem : d ∈ cls (col d).

    Lean, line 82
      have hdmem := (hcover d hd).2

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 82 at bc7b614c54a9 ↗

  19. hg have c.gcd d * A.max' hne = (840 : ℕ) * x.gcd y

    Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hg : c.gcd d * A.max' hne = (840 : ℕ) * x.gcd y.

    Uses library Nat.gcd_mul_right, Nat.gcd_mul_left.

    Lean, lines 85–86
      have hg : c.gcd d * A.max' hne = 840 * x.gcd y := by
    rw [← Nat.gcd_mul_right, ← hxc, ← hyd, Nat.gcd_mul_left]

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 85–86 at bc7b614c54a9 ↗

  20. 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 87
      have hxA : x ∈ A := (Finset.mem_erase.mp hx).2

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 87 at bc7b614c54a9 ↗

  21. 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 88
      have hyA : y ∈ A := (Finset.mem_erase.mp hy).2

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 88 at bc7b614c54a9 ↗

  22. s22 case

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

    Uses library absurd Anything follows from two contradictory hypotheses. .

    Lean, line 90
      · exact absurd h hcd

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 90 at bc7b614c54a9 ↗

  23. s23 case

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

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

    Lean, lines 91–94
      · refine ⟨x, hxA, y, hyA, toQ x y ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hxc] at h2
    omega

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 91–94 at bc7b614c54a9 ↗

    1. s23.h2 have (9 : ℕ) * c.gcd d * A.max' hne ≤ c * A.max' hne

      Leaves (9 : ℕ) * x.gcd y ≤ x, with h2 : (9 : ℕ) * c.gcd d * A.max' hne ≤ c * A.max' hne.

      Uses library Nat.mul_le_mul_right.

      Lean, line 92
          have h2 := Nat.mul_le_mul_right (A.max' hne) h

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 92 at bc7b614c54a9 ↗

  24. s24 case

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

    Uses library Exists.intro Existential introduction. , Nat.mul_assoc, Nat.gcd_comm.

    Lean, lines 95–99
      · refine ⟨y, hyA, x, hxA, toQ y x ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hyd] at h2
    rw [Nat.gcd_comm]
    omega

    targets/erdos-402/nodes/variant-892f5809/Proof.lean, lines 95–99 at bc7b614c54a9 ↗

    1. s24.h2 have (9 : ℕ) * c.gcd d * A.max' hne ≤ d * A.max' hne

      Leaves (9 : ℕ) * y.gcd x ≤ y, with h2 : (9 : ℕ) * c.gcd d * A.max' hne ≤ d * A.max' hne.

      Uses library Nat.mul_le_mul_right.

      Lean, line 96
          have h2 := Nat.mul_le_mul_right (A.max' hne) h

      targets/erdos-402/nodes/variant-892f5809/Proof.lean, line 96 at bc7b614c54a9 ↗

The proof in Lean (Proof.lean)

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

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-892f5809/Proof.lean, sha256 ed5033244e49.
import Mathlib
import Nodes.«variant-892f5809».Context

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

theorem Opn.erdos_402_card_nine :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 9 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A h0 hcard
  have toQ : ∀ a b : ℕ, 9 * a.gcd b ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
    intro a b hab
    have h9 : ((A.card : ℕ) : ℚ) = 9 := by rw [hcard]; norm_num
    rw [h9, le_div_iff₀ (by norm_num : (0 : ℚ) < 9)]
    exact_mod_cast (by omega : a.gcd b * 9 ≤ a)
  have hne : A.Nonempty := Finset.card_pos.mp (by omega)
  have hMA : A.max' hne ∈ A := Finset.max'_mem A hne
  have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero fun h => h0 (h ▸ hMA)
  by_cases hdirect : ∃ x ∈ A, 9 * (A.max' hne).gcd x ≤ A.max' hne
  · obtain ⟨x, hxA, hx⟩ := hdirect
    exact ⟨A.max' hne, hMA, x, hxA, toQ _ x hx⟩
  simp only [not_exists, not_and, not_le] at hdirect
  -- every other element x satisfies 840 x = c M with c = 840 j / k, 1 ≤ j < k ≤ 8
  have hval : ∀ x ∈ A.erase (A.max' hne), ∃ c ∈ [105, 120, 140, 168, 210, 240, 280, 315, 336, 360,
      420, 480, 504, 525, 560, 600, 630, 672, 700, 720, 735], 840 * x = c * A.max' hne := by
    intro x hx
    obtain ⟨hxM, hxA⟩ := Finset.mem_erase.mp hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero fun h => h0 (h ▸ hxA)
    have hxlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
    have hbig : A.max' hne < 9 * (A.max' hne).gcd x := hdirect x hxA
    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
    have hk9 : k < 9 := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    have hjk : j < k := by
      by_contra hc
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) (not_lt.mp hc)
      omega
    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 ⟨840 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega
  -- a colouring of the 21 values into 7 classes, each class pairwise good
  obtain ⟨cls, hcls⟩ : ∃ cls : ℕ → List ℕ, cls = fun i => [[420, 600], [210, 360, 672, 700],
      [120, 560, 630], [105, 240, 504], [280, 315, 480], [168, 525, 720], [140, 336, 735]].getD i [] :=
    ⟨_, rfl⟩
  obtain ⟨col, hcol⟩ : ∃ col : ℕ → ℕ, col = fun c => [[420, 600], [210, 360, 672, 700],
      [120, 560, 630], [105, 240, 504], [280, 315, 480], [168, 525, 720], [140, 336, 735]].findIdx
      (fun C => C.contains c) := ⟨_, rfl⟩
  have hcover : ∀ c ∈ ([105, 120, 140, 168, 210, 240, 280, 315, 336, 360, 420, 480, 504, 525, 560,
      600, 630, 672, 700, 720, 735] : List ℕ), col c < 7 ∧ c ∈ cls (col c) := by
    subst hcol hcls
    decide
  have hgood : ∀ i < 7, ∀ c ∈ cls i, ∀ d ∈ cls i, c = d ∨ 9 * c.gcd d ≤ c ∨ 9 * c.gcd d ≤ d := by
    subst hcls
    decide
  -- pigeonhole: eight other elements, seven classes
  have hmaps : ∀ x ∈ A.erase (A.max' hne), col (840 * x / A.max' hne) ∈ Finset.range 7 := by
    intro x hx
    obtain ⟨c, hc, hxc⟩ := hval x hx
    rw [Finset.mem_range, hxc, Nat.mul_div_cancel _ hMpos]
    exact (hcover c hc).1
  have hcard8 : (Finset.range 7).card < (A.erase (A.max' hne)).card := by
    rw [Finset.card_erase_of_mem hMA, hcard, Finset.card_range]
    norm_num
  obtain ⟨x, hx, y, hy, hxy, hxycol⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to hcard8 hmaps
  obtain ⟨c, hc, hxc⟩ := hval x hx
  obtain ⟨d, hd, hyd⟩ := hval y hy
  rw [hxc, hyd, Nat.mul_div_cancel _ hMpos, Nat.mul_div_cancel _ hMpos] at hxycol
  have hcd : c ≠ d := by
    rintro rfl
    exact hxy (by omega)
  have hcmem := (hcover c hc).2
  have hdmem := (hcover d hd).2
  rw [← hxycol] at hdmem
  -- transfer the good pair of values back to x and y
  have hg : c.gcd d * A.max' hne = 840 * x.gcd y := by
    rw [← Nat.gcd_mul_right, ← hxc, ← hyd, Nat.gcd_mul_left]
  have hxA : x ∈ A := (Finset.mem_erase.mp hx).2
  have hyA : y ∈ A := (Finset.mem_erase.mp hy).2
  rcases hgood (col c) (hcover c hc).1 c hcmem d hdmem with h | h | h
  · exact absurd h hcd
  · refine ⟨x, hxA, y, hyA, toQ x y ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hxc] at h2
    omega
  · refine ⟨y, hyA, x, hxA, toQ y x ?_⟩
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    rw [Nat.mul_assoc, hg, ← hyd] at h2
    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-892f5809».Context

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

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

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

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

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

Attestation: pass, 7 of 7 checks

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

Verdict pass, from attestations/000252.json.

Submitter
t0929-5
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/000252.json, merge commit bc7b614c54a9.

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

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 9 := ⟨Finset.Icc 1 9, 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-892f5809/Relation.lean, sha256 6bb5ce90926b.
-- 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 = 9 → ∃ 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 = 9 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 →