Graham's bound for |A| = 13

variant-9724698e

proved

A partial route to the problem.

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

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000304.json, merge commit 9732d83fda9e.

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 14
```
  have hpos : 0 < A.card := by omega
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 14 at 9732d83fda9e ↗
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 15
```
  have hne : A.Nonempty := Finset.card_pos.mp hpos
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 15 at 9732d83fda9e ↗
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 16–19
```
  have key : ∀ a b : ℕ, a.gcd b * A.card ≤ a → (a.gcd b : ℚ) ≤ (a / A.card : ℚ) := by
    intro a b h
    rw [le_div_iff₀ (by exact_mod_cast hpos)]
    exact_mod_cast h
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 16–19 at 9732d83fda9e ↗
s4 obtain ∃ (M : ℕ), M = A.max' hne
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with M : ℕ, hMdef : M = A.max' hne.
Uses library Exists.intro, rfl.
Lean, line 20
```
  obtain ⟨M, hMdef⟩ : ∃ M, M = A.max' hne := ⟨_, rfl⟩
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 20 at 9732d83fda9e ↗
hM have M ∈ A
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hM : M ∈ A.
Uses library Finset.max'_mem.
Lean, line 21
```
  have hM : M ∈ A := by rw [hMdef]; exact Finset.max'_mem A hne
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 21 at 9732d83fda9e ↗
hle have ∀ x ∈ A, x ≤ M
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hle : ∀ x ∈ A, x ≤ M.
Uses library Finset.le_max'.
Lean, lines 22–25
```
  have hle : ∀ x ∈ A, x ≤ M := by
    intro x hx
    rw [hMdef]
    exact Finset.le_max' A x hx
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 22–25 at 9732d83fda9e ↗
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 26
```
  have hMpos : 0 < M := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 26 at 9732d83fda9e ↗
s8 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 ⟨M, hM, x, hx, key M x (by rw [hn]; exact h)⟩
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 28–29 at 9732d83fda9e ↗
1. s8.s1 obtain ∃ x ∈ A, M.gcd x * (13 : ℕ) ≤ M
  Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with x : ℕ, hx : x ∈ A, h : M.gcd x * (13 : ℕ) ≤ M.
  Lean, line 28
  · obtain ⟨x, hx, h⟩ := hw
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 28 at 9732d83fda9e ↗
s9 obtain ∃ (S : List ℕ), S = let y := let y := let y := [(23760 : ℕ), (24255 : ℕ), (24640 : ℕ), (24948 : ℕ), (25200 : ℕ), (25410 : ℕ)]; (20160 : ℕ) :: (20790 : ℕ) :: (21560 : ℕ) :: (22176 : ℕ) :: (22680 : ℕ) :: (23100 : ℕ) :: y; let y := (16632 : ℕ) :: (17325 : ℕ) :: (17640 : ℕ) :: (18480 : ℕ) :: (19404 : ℕ) :: (19800 : ℕ) :: y; (13860 : ℕ) :: (15120 : ℕ) :: (15400 : ℕ) :: (15840 : ℕ) :: (16170 : ℕ) :: y; let y := let y := (10395 : ℕ) :: (11088 : ℕ) :: (11550 : ℕ) :: (11880 : ℕ) :: (12320 : ℕ) :: (12600 : ℕ) :: y; (7560 : ℕ) :: (7920 : ℕ) :: (8316 : ℕ) :: (9240 : ℕ) :: (10080 : ℕ) :: y; let y := (3960 : ℕ) :: (4620 : ℕ) :: (5040 : ℕ) :: (5544 : ℕ) :: (6160 : ℕ) :: (6930 : ℕ) :: y; (2310 : ℕ) :: (2520 : ℕ) :: (2772 : ℕ) :: (3080 : ℕ) :: (3465 : ℕ) :: y
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with S : List ℕ, hS : S = let y := let y := let y := [(23760 : ℕ), (24255 : ℕ), (24640 : ℕ), (24948 : ℕ), (25200 : ℕ), (25410 : ℕ)]; (20160 : ℕ) :: (20790 : ℕ) :: (21560 : ℕ) :: (22176 : ℕ) :: (22680 : ℕ) :: (23100 : ℕ) :: y; let y := (16632 : ℕ) :: (17325 : ℕ) :: (17640 : ℕ) :: (18480 : ℕ) :: (19404 : ℕ) :: (19800 : ℕ) :: y; (13860 : ℕ) :: (15120 : ℕ) :: (15400 : ℕ) :: (15840 : ℕ) :: (16170 : ℕ) :: y; let y := let y := (10395 : ℕ) :: (11088 : ℕ) :: (11550 : ℕ) :: (11880 : ℕ) :: (12320 : ℕ) :: (12600 : ℕ) :: y; (7560 : ℕ) :: (7920 : ℕ) :: (8316 : ℕ) :: (9240 : ℕ) :: (10080 : ℕ) :: y; let y := (3960 : ℕ) :: (4620 : ℕ) :: (5040 : ℕ) :: (5544 : ℕ) :: (6160 : ℕ) :: (6930 : ℕ) :: y; (2310 : ℕ) :: (2520 : ℕ) :: (2772 : ℕ) :: (3080 : ℕ) :: (3465 : ℕ) :: y.
Uses library List, Exists.intro, rfl.
Lean, line 31
```
  obtain ⟨S, hS⟩ : ∃ S : List ℕ, S = [2310, 2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11550, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16170, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200, 25410] := ⟨_, rfl⟩
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 31 at 9732d83fda9e ↗
s10 obtain ∃ (C : List (List ℕ)), C = [[(13860 : ℕ), (17640 : ℕ), (24640 : ℕ)], [(9240 : ℕ), (15120 : ℕ), (17325 : ℕ), (24948 : ℕ)], [(6930 : ℕ), (15400 : ℕ), (22176 : ℕ), (22680 : ℕ), (23760 : ℕ)], [(3465 : ℕ), (7560 : ℕ), (18480 : ℕ), (19404 : ℕ), (19800 : ℕ)], [(4620 : ℕ), (12600 : ℕ), (15840 : ℕ), (16632 : ℕ), (21560 : ℕ)], [(3960 : ℕ), (11088 : ℕ), (20160 : ℕ), (20790 : ℕ)], [(2310 : ℕ), (5040 : ℕ), (8316 : ℕ), (12320 : ℕ), (24255 : ℕ)], [(5544 : ℕ), (10080 : ℕ), (11550 : ℕ), (11880 : ℕ)], [(2520 : ℕ), (6160 : ℕ), (10395 : ℕ), (23100 : ℕ)], [(2772 : ℕ), (7920 : ℕ), (16170 : ℕ), (25200 : ℕ)], [(3080 : ℕ), (25410 : ℕ)]]
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with C : List (List ℕ), hC : C = [[(13860 : ℕ), (17640 : ℕ), (24640 : ℕ)], [(9240 : ℕ), (15120 : ℕ), (17325 : ℕ), (24948 : ℕ)], [(6930 : ℕ), (15400 : ℕ), (22176 : ℕ), (22680 : ℕ), (23760 : ℕ)], [(3465 : ℕ), (7560 : ℕ), (18480 : ℕ), (19404 : ℕ), (19800 : ℕ)], [(4620 : ℕ), (12600 : ℕ), (15840 : ℕ), (16632 : ℕ), (21560 : ℕ)], [(3960 : ℕ), (11088 : ℕ), (20160 : ℕ), (20790 : ℕ)], [(2310 : ℕ), (5040 : ℕ), (8316 : ℕ), (12320 : ℕ), (24255 : ℕ)], [(5544 : ℕ), (10080 : ℕ), (11550 : ℕ), (11880 : ℕ)], [(2520 : ℕ), (6160 : ℕ), (10395 : ℕ), (23100 : ℕ)], [(2772 : ℕ), (7920 : ℕ), (16170 : ℕ), (25200 : ℕ)], [(3080 : ℕ), (25410 : ℕ)]].
Uses library List, Exists.intro, rfl.
Lean, line 32
```
  obtain ⟨C, hC⟩ : ∃ C : List (List ℕ), C = [[13860, 17640, 24640], [9240, 15120, 17325, 24948], [6930, 15400, 22176, 22680, 23760], [3465, 7560, 18480, 19404, 19800], [4620, 12600, 15840, 16632, 21560], [3960, 11088, 20160, 20790], [2310, 5040, 8316, 12320, 24255], [5544, 10080, 11550, 11880], [2520, 6160, 10395, 23100], [2772, 7920, 16170, 25200], [3080, 25410]] := ⟨_, rfl⟩
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 32 at 9732d83fda9e ↗
P1 have ∀ k < (13 : ℕ), ∀ j < k, (0 : ℕ) < j → k ∣ (27720 : ℕ) ∧ (27720 : ℕ) / k * j ∈ S
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with P1 : ∀ k < (13 : ℕ), ∀ j < k, (0 : ℕ) < j → k ∣ (27720 : ℕ) ∧ (27720 : ℕ) / k * j ∈ S.
Lean, lines 33–35
```
  have P1 : ∀ k, k < 13 → ∀ j, j < k → 0 < j → k ∣ 27720 ∧ 27720 / k * j ∈ S := by
    subst hS
    decide
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 33–35 at 9732d83fda9e ↗
P3 have ∀ a ∈ S, List.findIdx (fun (l : List ℕ) => l.contains a) C < (11 : ℕ) ∧ a ∈ C.getD (List.findIdx (fun (l : List ℕ) => l.contains a) C) []
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with P3 : ∀ a ∈ S, List.findIdx (fun (l : List ℕ) => l.contains a) C < (11 : ℕ) ∧ a ∈ C.getD (List.findIdx (fun (l : List ℕ) => l.contains a) C) [].
Lean, lines 36–39
```
  have P3 : ∀ a ∈ S, C.findIdx (fun l => l.contains a) < 11 ∧
      a ∈ C.getD (C.findIdx (fun l => l.contains a)) [] := by
    subst hS hC
    decide
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 36–39 at 9732d83fda9e ↗
P2 have ∀ i < (11 : ℕ), ∀ a ∈ C.getD i [], ∀ b ∈ C.getD i [], a ≠ b → (13 : ℕ) * a.gcd b ≤ a ∨ (13 : ℕ) * a.gcd b ≤ b
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with P2 : ∀ i < (11 : ℕ), ∀ a ∈ C.getD i [], ∀ b ∈ C.getD i [], a ≠ b → (13 : ℕ) * a.gcd b ≤ a ∨ (13 : ℕ) * a.gcd b ≤ b.
Lean, lines 40–43
```
  have P2 : ∀ i, i < 11 → ∀ a ∈ C.getD i [], ∀ b ∈ C.getD i [], a ≠ b →
      13 * a.gcd b ≤ a ∨ 13 * a.gcd b ≤ b := by
    subst hC
    decide
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 40–43 at 9732d83fda9e ↗
forms have ∀ x ∈ A.erase M, ∃ a ∈ S, (27720 : ℕ) * x = a * M
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with forms : ∀ x ∈ A.erase M, ∃ a ∈ S, (27720 : ℕ) * x = a * M.
Uses library Finset.mem_erase, Exists.intro, Nat.mul_div_cancel_left.
Lean, lines 44–76
```
  have forms : ∀ x ∈ A.erase M, ∃ a ∈ S, 27720 * x = a * M := by
    intro x hx
    rw [Finset.mem_erase] at hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx.2))
    have hlt : x < M := lt_of_le_of_ne (hle x hx.2) hx.1
    have hg := hw x hx.2
    have hd1 := Nat.gcd_dvd_left M x
    have hd2 := Nat.gcd_dvd_right M x
    have hgpos : 0 < M.gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    generalize M.gcd x = g at hg hd1 hd2 hgpos
    obtain ⟨k, hk⟩ := hd1
    obtain ⟨j, hj⟩ := hd2
    have hk13 : k < 13 := by
      by_contra hh
      push Not at hh
      have := Nat.mul_le_mul_left g hh
      omega
    have hjk : j < k := by
      by_contra hh
      push Not at hh
      have := Nat.mul_le_mul_left g hh
      omega
    have hj1 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · subst h
        omega
      · exact h
    obtain ⟨hdvd, hmem⟩ := P1 k hk13 j hjk hj1
    refine ⟨27720 / k * j, hmem, ?_⟩
    obtain ⟨q, hq⟩ := hdvd
    have hkpos : 0 < k := by omega
    rw [hq, Nat.mul_div_cancel_left q hkpos, hk, hj]
    ring
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 44–76 at 9732d83fda9e ↗
1. forms.hxpos have (0 : ℕ) < x
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hxpos : (0 : ℕ) < x.
  Uses library Nat.pos_of_ne_zero.
  Lean, line 47
  have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx.2))
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 47 at 9732d83fda9e ↗
2. forms.hlt have x < M
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hlt : x < M.
  Uses library lt_of_le_of_ne.
  Lean, line 48
  have hlt : x < M := lt_of_le_of_ne (hle x hx.2) hx.1
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 48 at 9732d83fda9e ↗
3. forms.hg have M < M.gcd x * (13 : ℕ)
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hg : M < M.gcd x * (13 : ℕ).
  Lean, line 49
  have hg := hw x hx.2
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 49 at 9732d83fda9e ↗
4. forms.hd1 have M.gcd x ∣ M
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hd1 : M.gcd x ∣ M.
  Uses library Nat.gcd_dvd_left.
  Lean, line 50
  have hd1 := Nat.gcd_dvd_left M x
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 50 at 9732d83fda9e ↗
5. forms.hd2 have M.gcd x ∣ x
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hd2 : M.gcd x ∣ x.
  Uses library Nat.gcd_dvd_right.
  Lean, line 51
  have hd2 := Nat.gcd_dvd_right M x
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 51 at 9732d83fda9e ↗
6. forms.hgpos have (0 : ℕ) < M.gcd x
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hgpos : (0 : ℕ) < M.gcd x.
  Uses library Nat.gcd_pos_of_pos_right.
  Lean, line 52
  have hgpos : 0 < M.gcd x := Nat.gcd_pos_of_pos_right _ hxpos
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 52 at 9732d83fda9e ↗
7. forms.s7 obtain g ∣ M
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with k : ℕ, hk : M = g * k.
  Lean, line 54
  obtain ⟨k, hk⟩ := hd1
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 54 at 9732d83fda9e ↗
8. forms.s8 obtain g ∣ x
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with j : ℕ, hj : x = g * j.
  Lean, line 55
  obtain ⟨j, hj⟩ := hd2
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 55 at 9732d83fda9e ↗
9. forms.hk13 have k < (13 : ℕ)
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hk13 : k < (13 : ℕ).
  Uses library Not.
  Lean, lines 56–60
  have hk13 : k < 13 := by by_contra hh push Not at hh have := Nat.mul_le_mul_left g hh omega
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 56–60 at 9732d83fda9e ↗
  forms.hk13.this have g * (13 : ℕ) ≤ g * k
  Leaves False, with this : g * (13 : ℕ) ≤ g * k.
  Uses library Nat.mul_le_mul_left.
  Lean, line 59
  have := Nat.mul_le_mul_left g hh
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 59 at 9732d83fda9e ↗
10. forms.hjk have j < k
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hjk : j < k.
  Uses library Not.
  Lean, lines 61–65
  have hjk : j < k := by by_contra hh push Not at hh have := Nat.mul_le_mul_left g hh omega
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 61–65 at 9732d83fda9e ↗
  forms.hjk.this have g * k ≤ g * j
  Leaves False, with this : g * k ≤ g * j.
  Uses library Nat.mul_le_mul_left.
  Lean, line 64
  have := Nat.mul_le_mul_left g hh
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 64 at 9732d83fda9e ↗
11. forms.hj1 have (0 : ℕ) < j
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hj1 : (0 : ℕ) < j.
  Uses library Nat.eq_zero_or_pos.
  Lean, lines 66–70
  have hj1 : 0 < j := by rcases Nat.eq_zero_or_pos j with h | h · subst h omega · exact h
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 66–70 at 9732d83fda9e ↗
  forms.hj1.s1 case
  Leaves (0 : ℕ) < j.
  Lean, lines 68–69
  · subst h omega
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 68–69 at 9732d83fda9e ↗
  forms.hj1.s2 case
  Leaves (0 : ℕ) < j.
  Lean, line 70
  · exact h
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 70 at 9732d83fda9e ↗
12. forms.s12 obtain k ∣ (27720 : ℕ) ∧ (27720 : ℕ) / k * j ∈ S
  Leaves ∃ a ∈ S, (27720 : ℕ) * x = a * M, with hdvd : k ∣ (27720 : ℕ), hmem : (27720 : ℕ) / k * j ∈ S.
  Lean, line 71
  obtain ⟨hdvd, hmem⟩ := P1 k hk13 j hjk hj1
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 71 at 9732d83fda9e ↗
13. forms.s13 obtain k ∣ (27720 : ℕ)
  Leaves (27720 : ℕ) * x = (27720 : ℕ) / k * j * M, with q : ℕ, hq : (27720 : ℕ) = k * q.
  Lean, line 73
  obtain ⟨q, hq⟩ := hdvd
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 73 at 9732d83fda9e ↗
14. forms.hkpos have (0 : ℕ) < k routine: omega
  Leaves (27720 : ℕ) * x = (27720 : ℕ) / k * j * M, with hkpos : (0 : ℕ) < k.
  Lean, line 74
  have hkpos : 0 < k := by omega
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 74 at 9732d83fda9e ↗
hcard have (A.erase M).card = (12 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcard : (A.erase M).card = (12 : ℕ).
Uses library Finset.card_erase_of_mem.
Lean, lines 77–78
```
  have hcard : (A.erase M).card = 12 := by
    rw [Finset.card_erase_of_mem hM, hn]
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 77–78 at 9732d83fda9e ↗
hmaps have ∀ x ∈ A.erase M, List.findIdx (fun (l : List ℕ) => l.contains ((27720 : ℕ) * x / M)) C ∈ Finset.range (11 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase M, List.findIdx (fun (l : List ℕ) => l.contains ((27720 : ℕ) * x / M)) C ∈ Finset.range (11 : ℕ).
Uses library Finset.range, Finset.mem_range, Nat.mul_div_cancel.
Lean, lines 79–83
```
  have hmaps : ∀ x ∈ A.erase M, C.findIdx (fun l => l.contains (27720 * x / M)) ∈ Finset.range 11 := by
    intro x hx
    obtain ⟨a, ha, hax⟩ := forms x hx
    rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
    exact (P3 a ha).1
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 79–83 at 9732d83fda9e ↗
1. hmaps.s1 obtain ∃ a ∈ S, (27720 : ℕ) * x = a * M
  Leaves List.findIdx (fun (l : List ℕ) => l.contains ((27720 : ℕ) * x / M)) C ∈ Finset.range (11 : ℕ), with a : ℕ, ha : a ∈ S, hax : (27720 : ℕ) * x = a * M.
  Lean, line 81
  obtain ⟨a, ha, hax⟩ := forms x hx
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 81 at 9732d83fda9e ↗
s17 obtain ∃ x ∈ A.erase M, ∃ y ∈ A.erase M, x ≠ y ∧ List.findIdx (fun (l : List ℕ) => l.contains ((27720 : ℕ) * x / M)) C = List.findIdx (fun (l : List ℕ) => l.contains ((27720 : ℕ) * y / M)) C
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 : List.findIdx (fun (l : List ℕ) => l.contains ((27720 : ℕ) * x / M)) C = List.findIdx (fun (l : List ℕ) => l.contains ((27720 : ℕ) * y / M)) C.
Uses library Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.card_range.
Lean, lines 84–85
```
  obtain ⟨x, hx, y, hy, hxy, hc⟩ :=
    Finset.exists_ne_map_eq_of_card_lt_of_maps_to (by rw [hcard, Finset.card_range]; norm_num) hmaps
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 84–85 at 9732d83fda9e ↗
s18 obtain ∃ a ∈ S, (27720 : ℕ) * x = a * M
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with a : ℕ, ha : a ∈ S, hax : (27720 : ℕ) * x = a * M.
Lean, line 86
```
  obtain ⟨a, ha, hax⟩ := forms x hx
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 86 at 9732d83fda9e ↗
s19 obtain ∃ a ∈ S, (27720 : ℕ) * y = a * M
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with b : ℕ, hb : b ∈ S, hby : (27720 : ℕ) * y = b * M.
Lean, line 87
```
  obtain ⟨b, hb, hby⟩ := forms y hy
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 87 at 9732d83fda9e ↗
hab have a ≠ b
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hab : a ≠ b.
Lean, lines 89–93
```
  have hab : a ≠ b := by
    intro h
    subst h
    apply hxy
    omega
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 89–93 at 9732d83fda9e ↗
s21 obtain List.findIdx (fun (l : List ℕ) => l.contains a) C < (11 : ℕ) ∧ a ∈ C.getD (List.findIdx (fun (l : List ℕ) => l.contains a) C) []
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hi : List.findIdx (fun (l : List ℕ) => l.contains a) C < (11 : ℕ), hai : a ∈ C.getD (List.findIdx (fun (l : List ℕ) => l.contains a) C) [].
Lean, line 94
```
  obtain ⟨hi, hai⟩ := P3 a ha
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 94 at 9732d83fda9e ↗
s22 obtain List.findIdx (fun (l : List ℕ) => l.contains b) C < (11 : ℕ) ∧ b ∈ C.getD (List.findIdx (fun (l : List ℕ) => l.contains b) C) []
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with left✝ : List.findIdx (fun (l : List ℕ) => l.contains b) C < (11 : ℕ), hbi : b ∈ C.getD (List.findIdx (fun (l : List ℕ) => l.contains b) C) [].
Lean, line 95
```
  obtain ⟨_, hbi⟩ := P3 b hb
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 95 at 9732d83fda9e ↗
hgcd have a.gcd b * M = (27720 : ℕ) * x.gcd y
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgcd : a.gcd b * M = (27720 : ℕ) * x.gcd y.
Uses library Nat.gcd_mul_right.
Lean, lines 97–100
```
  have hgcd : a.gcd b * M = 27720 * x.gcd y := by
    have h1 : Nat.gcd (27720 * x) (27720 * y) = 27720 * x.gcd y := Nat.gcd_mul_left 27720 x y
    rw [hax, hby, Nat.gcd_mul_right] at h1
    exact h1
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 97–100 at 9732d83fda9e ↗
1. hgcd.h1 have ((27720 : ℕ) * x).gcd ((27720 : ℕ) * y) = (27720 : ℕ) * x.gcd y
  Leaves a.gcd b * M = (27720 : ℕ) * x.gcd y, with h1 : ((27720 : ℕ) * x).gcd ((27720 : ℕ) * y) = (27720 : ℕ) * x.gcd y.
  Uses library Nat.gcd, Nat.gcd_mul_left.
  Lean, line 98
  have h1 : Nat.gcd (27720 * x) (27720 * y) = 27720 * x.gcd y := Nat.gcd_mul_left 27720 x y
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 98 at 9732d83fda9e ↗
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 101
```
  have hxA := (Finset.mem_erase.mp hx).2
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 101 at 9732d83fda9e ↗
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 102
```
  have hyA := (Finset.mem_erase.mp hy).2
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 102 at 9732d83fda9e ↗
s26 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro, Nat.le_of_mul_le_mul_right.
Lean, lines 104–108
```
  · refine ⟨x, hxA, y, hyA, key x y ?_⟩
    rw [hn]
    have h2 := Nat.mul_le_mul_right M h
    have h3 : x.gcd y * 13 * 27720 ≤ x * 27720 := by nlinarith
    exact Nat.le_of_mul_le_mul_right h3 (by norm_num)
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 104–108 at 9732d83fda9e ↗
1. s26.h2 have (13 : ℕ) * a.gcd b * M ≤ a * M
  Leaves x.gcd y * (13 : ℕ) ≤ x, with h2 : (13 : ℕ) * a.gcd b * M ≤ a * M.
  Uses library Nat.mul_le_mul_right.
  Lean, line 106
  have h2 := Nat.mul_le_mul_right M h
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 106 at 9732d83fda9e ↗
2. s26.h3 have x.gcd y * (13 : ℕ) * (27720 : ℕ) ≤ x * (27720 : ℕ) routine: nlinarith
  Leaves x.gcd y * (13 : ℕ) ≤ x, with h3 : x.gcd y * (13 : ℕ) * (27720 : ℕ) ≤ x * (27720 : ℕ).
  Lean, line 107
  have h3 : x.gcd y * 13 * 27720 ≤ x * 27720 := by nlinarith
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 107 at 9732d83fda9e ↗
s27 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_right.
Lean, lines 109–113
```
  · refine ⟨y, hyA, x, hxA, key y x ?_⟩
    rw [hn, Nat.gcd_comm]
    have h2 := Nat.mul_le_mul_right M h
    have h3 : x.gcd y * 13 * 27720 ≤ y * 27720 := by nlinarith
    exact Nat.le_of_mul_le_mul_right h3 (by norm_num)
```
targets/erdos-402/nodes/variant-9724698e/Proof.lean, lines 109–113 at 9732d83fda9e ↗
1. s27.h2 have (13 : ℕ) * a.gcd b * M ≤ b * M
  Leaves x.gcd y * (13 : ℕ) ≤ y, with h2 : (13 : ℕ) * a.gcd b * M ≤ b * M.
  Uses library Nat.mul_le_mul_right.
  Lean, line 111
  have h2 := Nat.mul_le_mul_right M h
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 111 at 9732d83fda9e ↗
2. s27.h3 have x.gcd y * (13 : ℕ) * (27720 : ℕ) ≤ y * (27720 : ℕ) routine: nlinarith
  Leaves x.gcd y * (13 : ℕ) ≤ y, with h3 : x.gcd y * (13 : ℕ) * (27720 : ℕ) ≤ y * (27720 : ℕ).
  Lean, line 112
  have h3 : x.gcd y * 13 * 27720 ≤ y * 27720 := by nlinarith
  targets/erdos-402/nodes/variant-9724698e/Proof.lean, line 112 at 9732d83fda9e ↗

The proof in Lean (Proof.lean)

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

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-9724698e/Proof.lean, sha256 895d575caea1.

import Mathlib
import Nodes.«variant-9724698e».Context

/-! Graham's gcd conjecture (Erdős problem 402) for thirteen-element sets. Let M be the largest
element. If some x has gcd(M, x) ≤ M/13 the pair (M, x) works; otherwise each of the other twelve
elements is x = (j/k)·M with 1 ≤ j < k ≤ 12, so v(x) = 27720·x/M (27720 = lcm(1..12)) is one of 45
integers. Those 45 values split into 11 classes in each of which any two distinct values c, d have
13·gcd(c, d) ≤ c or ≤ d. Twelve elements in eleven classes put two in one class, and
gcd(x, y)·27720 = gcd(v(x), v(y))·M carries the bound back to x and y. -/

theorem Opn.erdos_402_card_thirteen :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 13 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A hA hn
  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
  obtain ⟨M, hMdef⟩ : ∃ M, M = A.max' hne := ⟨_, rfl⟩
  have hM : M ∈ A := by rw [hMdef]; exact Finset.max'_mem A hne
  have hle : ∀ x ∈ A, x ≤ M := by
    intro x hx
    rw [hMdef]
    exact Finset.le_max' A x hx
  have hMpos : 0 < M := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))
  by_cases hw : ∃ x ∈ A, M.gcd x * 13 ≤ M
  · obtain ⟨x, hx, h⟩ := hw
    exact ⟨M, hM, x, hx, key M x (by rw [hn]; exact h)⟩
  push Not at hw
  obtain ⟨S, hS⟩ : ∃ S : List ℕ, S = [2310, 2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11550, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16170, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200, 25410] := ⟨_, rfl⟩
  obtain ⟨C, hC⟩ : ∃ C : List (List ℕ), C = [[13860, 17640, 24640], [9240, 15120, 17325, 24948], [6930, 15400, 22176, 22680, 23760], [3465, 7560, 18480, 19404, 19800], [4620, 12600, 15840, 16632, 21560], [3960, 11088, 20160, 20790], [2310, 5040, 8316, 12320, 24255], [5544, 10080, 11550, 11880], [2520, 6160, 10395, 23100], [2772, 7920, 16170, 25200], [3080, 25410]] := ⟨_, rfl⟩
  have P1 : ∀ k, k < 13 → ∀ j, j < k → 0 < j → k ∣ 27720 ∧ 27720 / k * j ∈ S := by
    subst hS
    decide
  have P3 : ∀ a ∈ S, C.findIdx (fun l => l.contains a) < 11 ∧
      a ∈ C.getD (C.findIdx (fun l => l.contains a)) [] := by
    subst hS hC
    decide
  have P2 : ∀ i, i < 11 → ∀ a ∈ C.getD i [], ∀ b ∈ C.getD i [], a ≠ b →
      13 * a.gcd b ≤ a ∨ 13 * a.gcd b ≤ b := by
    subst hC
    decide
  have forms : ∀ x ∈ A.erase M, ∃ a ∈ S, 27720 * x = a * M := by
    intro x hx
    rw [Finset.mem_erase] at hx
    have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx.2))
    have hlt : x < M := lt_of_le_of_ne (hle x hx.2) hx.1
    have hg := hw x hx.2
    have hd1 := Nat.gcd_dvd_left M x
    have hd2 := Nat.gcd_dvd_right M x
    have hgpos : 0 < M.gcd x := Nat.gcd_pos_of_pos_right _ hxpos
    generalize M.gcd x = g at hg hd1 hd2 hgpos
    obtain ⟨k, hk⟩ := hd1
    obtain ⟨j, hj⟩ := hd2
    have hk13 : k < 13 := by
      by_contra hh
      push Not at hh
      have := Nat.mul_le_mul_left g hh
      omega
    have hjk : j < k := by
      by_contra hh
      push Not at hh
      have := Nat.mul_le_mul_left g hh
      omega
    have hj1 : 0 < j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · subst h
        omega
      · exact h
    obtain ⟨hdvd, hmem⟩ := P1 k hk13 j hjk hj1
    refine ⟨27720 / k * j, hmem, ?_⟩
    obtain ⟨q, hq⟩ := hdvd
    have hkpos : 0 < k := by omega
    rw [hq, Nat.mul_div_cancel_left q hkpos, hk, hj]
    ring
  have hcard : (A.erase M).card = 12 := by
    rw [Finset.card_erase_of_mem hM, hn]
  have hmaps : ∀ x ∈ A.erase M, C.findIdx (fun l => l.contains (27720 * x / M)) ∈ Finset.range 11 := by
    intro x hx
    obtain ⟨a, ha, hax⟩ := forms x hx
    rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
    exact (P3 a ha).1
  obtain ⟨x, hx, y, hy, hxy, hc⟩ :=
    Finset.exists_ne_map_eq_of_card_lt_of_maps_to (by rw [hcard, Finset.card_range]; norm_num) hmaps
  obtain ⟨a, ha, hax⟩ := forms x hx
  obtain ⟨b, hb, hby⟩ := forms y hy
  simp only [hax, hby, Nat.mul_div_cancel _ hMpos] at hc
  have hab : a ≠ b := by
    intro h
    subst h
    apply hxy
    omega
  obtain ⟨hi, hai⟩ := P3 a ha
  obtain ⟨_, hbi⟩ := P3 b hb
  rw [← hc] at hbi
  have hgcd : a.gcd b * M = 27720 * x.gcd y := by
    have h1 : Nat.gcd (27720 * x) (27720 * y) = 27720 * x.gcd y := Nat.gcd_mul_left 27720 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 P2 _ hi a hai b hbi hab with h | h
  · refine ⟨x, hxA, y, hyA, key x y ?_⟩
    rw [hn]
    have h2 := Nat.mul_le_mul_right M h
    have h3 : x.gcd y * 13 * 27720 ≤ x * 27720 := by nlinarith
    exact Nat.le_of_mul_le_mul_right h3 (by norm_num)
  · refine ⟨y, hyA, x, hxA, key y x ?_⟩
    rw [hn, Nat.gcd_comm]
    have h2 := Nat.mul_le_mul_right M h
    have h3 : x.gcd y * 13 * 27720 ≤ y * 27720 := by nlinarith
    exact Nat.le_of_mul_le_mul_right h3 (by norm_num)

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-9724698e».Context

/-! Graham's gcd conjecture (Erdős problem 402) for thirteen-element sets. Let M be the largest
element. If some x has gcd(M, x) ≤ M/13 the pair (M, x) works; otherwise each of the other twelve
elements is x = (j/k)·M with 1 ≤ j < k ≤ 12, so v(x) = 27720·x/M (27720 = lcm(1..12)) is one of 45
integers. Those 45 values split into 11 classes in each of which any two distinct values c, d have
13·gcd(c, d) ≤ c or ≤ d. Twelve elements in eleven classes put two in one class, and
gcd(x, y)·27720 = gcd(v(x), v(y))·M carries the bound back to x and y. -/

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

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

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

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000304.json, merge commit 9732d83fda9e.

Verdict pass, from attestations/000304.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/000304.json, merge commit 9732d83fda9e.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/variant-9724698e/Witness.lean, sha256 219526a7d17d.

import Mathlib

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 13 :=
  ⟨Finset.Icc 1 13, by simp, by simp⟩

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-9724698e/Relation.lean, sha256 cfbce74fb04c.

-- 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 = 13 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) :=
  fun h A hA hn => 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 = 13 is a hypothesis, so the rational division is by 13, never by zero.

How to read this page

How to read a statement’s page →