Graham's bound for |A| = 12

variant-11152e83

proved

A partial route to the problem.

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

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000299.json, merge commit 2de0bec6584f.

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 13
```
  have hpos : 0 < A.card := by omega
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 13 at 2de0bec6584f ↗
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 14
```
  have hne : A.Nonempty := Finset.card_pos.mp hpos
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 14 at 2de0bec6584f ↗
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 15–18
```
  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-11152e83/Proof.lean, lines 15–18 at 2de0bec6584f ↗
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 19
```
  have hM : A.max' hne ∈ A := Finset.max'_mem A hne
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 19 at 2de0bec6584f ↗
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 20
```
  have hMpos : 0 < A.max' hne := Nat.pos_of_ne_zero (fun h => hA (h ▸ hM))
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 20 at 2de0bec6584f ↗
s6 case
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ).
Uses library Exists.intro.
Lean, lines 22–23
```
  · obtain ⟨x, hx, h⟩ := hw
    exact ⟨_, hM, x, hx, key _ x (by rw [hn]; exact h)⟩
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 22–23 at 2de0bec6584f ↗
1. s6.s1 obtain ∃ x ∈ A, (A.max' hne).gcd x * (12 : ℕ) ≤ 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 * (12 : ℕ) ≤ A.max' hne.
  Lean, line 22
  · obtain ⟨x, hx, h⟩ := hw
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 22 at 2de0bec6584f ↗
forms have printed form did not read back: shown as its Lean lines only
```
  have forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), 27720 * x = a * A.max' hne := 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 < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1
    have hg := hw x hx.2
    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 hkN : k < 12 := by
      by_contra hh
      push_neg at hh
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh
      omega
    have hjk : j < k := by
      by_contra hh
      push_neg at hh
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh
      omega
    have hj1 : 1 ≤ j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · subst h
        omega
      · exact h
    refine ⟨27720 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 25–51 at 2de0bec6584f ↗
1. forms.hxpos have printed form did not read back: shown as its Lean lines only
  have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hx.2))
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 28 at 2de0bec6584f ↗
2. forms.hlt have printed form did not read back: shown as its Lean lines only
  have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 29 at 2de0bec6584f ↗
3. forms.hg have printed form did not read back: shown as its Lean lines only
  have hg := hw x hx.2
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 30 at 2de0bec6584f ↗
4. forms.s4 obtain printed form did not read back: shown as its Lean lines only
  obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 31 at 2de0bec6584f ↗
5. forms.s5 obtain printed form did not read back: shown as its Lean lines only
  obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 32 at 2de0bec6584f ↗
6. forms.hgpos have printed form did not read back: shown as its Lean lines only
  have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 33 at 2de0bec6584f ↗
7. forms.hkN have printed form did not read back: shown as its Lean lines only
  have hkN : k < 12 := by by_contra hh push_neg at hh have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh omega
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 34–38 at 2de0bec6584f ↗
  forms.hkN.this have (A.max' hne).gcd x * (12 : ℕ) ≤ (A.max' hne).gcd x * k
  Leaves False, with this : (A.max' hne).gcd x * (12 : ℕ) ≤ (A.max' hne).gcd x * k.
  Uses library Nat.mul_le_mul_left.
  Lean, line 37
  have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 37 at 2de0bec6584f ↗
8. forms.hjk have printed form did not read back: shown as its Lean lines only
  have hjk : j < k := by by_contra hh push_neg at hh have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh omega
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 39–43 at 2de0bec6584f ↗
  forms.hjk.this have (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j
  Leaves False, with this : (A.max' hne).gcd x * k ≤ (A.max' hne).gcd x * j.
  Uses library Nat.mul_le_mul_left.
  Lean, line 42
  have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 42 at 2de0bec6584f ↗
9. forms.hj1 have printed form did not read back: shown as its Lean lines only
  have hj1 : 1 ≤ j := by rcases Nat.eq_zero_or_pos j with h | h · subst h omega · exact h
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 44–48 at 2de0bec6584f ↗
  forms.hj1.s1 case
  Leaves (1 : ℕ) ≤ j.
  Lean, lines 46–47
  · subst h omega
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 46–47 at 2de0bec6584f ↗
  forms.hj1.s2 case
  Leaves (1 : ℕ) ≤ j.
  Lean, line 48
  · exact h
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 48 at 2de0bec6584f ↗
10. forms.s10 case printed form did not read back: shown as its Lean lines only
  · interval_cases k <;> interval_cases j <;> decide
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 50 at 2de0bec6584f ↗
11. forms.s11 case
  Leaves (27720 : ℕ) * x = (27720 : ℕ) * j / k * A.max' hne.
  Lean, line 51
  · interval_cases k <;> interval_cases j <;> omega
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 51 at 2de0bec6584f ↗
hcard have (A.erase (A.max' hne)).card = (11 : ℕ)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hcard : (A.erase (A.max' hne)).card = (11 : ℕ).
Uses library Finset.card_erase_of_mem.
Lean, lines 52–53
```
  have hcard : (A.erase (A.max' hne)).card = 11 := by
    rw [Finset.card_erase_of_mem hM, hn]
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 52–53 at 2de0bec6584f ↗

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

  have hS : ∀ a ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) a < 10 := by decide

targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 54 at 2de0bec6584f ↗

hmaps have ∀ x ∈ A.erase (A.max' hne), (fun (a : ℕ) => if a = (2520 : ℕ) then (2 : ℕ) else if a = (2772 : ℕ) then (7 : ℕ) else if a = (3080 : ℕ) then (6 : ℕ) else if a = (3465 : ℕ) then (9 : ℕ) else if a = (3960 : ℕ) then (8 : ℕ) else if a = (4620 : ℕ) then (5 : ℕ) else if a = (5040 : ℕ) then (5 : ℕ) else if a = (5544 : ℕ) then (4 : ℕ) else if a = (6160 : ℕ) then (7 : ℕ) else if a = (6930 : ℕ) then (3 : ℕ) else if a = (7560 : ℕ) then (3 : ℕ) else if a = (7920 : ℕ) then (9 : ℕ) else if a = (8316 : ℕ) then (2 : ℕ) else if a = (9240 : ℕ) then (1 : ℕ) else if a = (10080 : ℕ) then (1 : ℕ) else if a = (10395 : ℕ) then (6 : ℕ) else if a = (11088 : ℕ) then (6 : ℕ) else if a = (11880 : ℕ) then (7 : ℕ) else if a = (12320 : ℕ) then (4 : ℕ) else if a = (12600 : ℕ) then (4 : ℕ) else if a = (13860 : ℕ) then (0 : ℕ) else (truncated)
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hmaps : ∀ x ∈ A.erase (A.max' hne), (fun (a : ℕ) => if a = (2520 : ℕ) then (2 : ℕ) else if a = (2772 : ℕ) then (7 : ℕ) else if a = (3080 : ℕ) then (6 : ℕ) else if a = (3465 : ℕ) then (9 : ℕ) else if a = (3960 : ℕ) then (8 : ℕ) else if a = (4620 : ℕ) then (5 : ℕ) else if a = (5040 : ℕ) then (5 : ℕ) else if a = (5544 : ℕ) then (4 : ℕ) else if a = (6160 : ℕ) then (7 : ℕ) else if a = (6930 : ℕ) then (3 : ℕ) else if a = (7560 : ℕ) then (3 : ℕ) else if a = (7920 : ℕ) then (9 : ℕ) else if a = (8316 : ℕ) then (2 : ℕ) else if a = (9240 : ℕ) then (1 : ℕ) else if a = (10080 : ℕ) then (1 : ℕ) else if a = (10395 : ℕ) then (6 : ℕ) else if a = (11088 : ℕ) then (6 : ℕ) else if a = (11880 : ℕ) then (7 : ℕ) else if a = (12320 : ℕ) then (4 : ℕ) else if a = (12600 : ℕ) then (4 : ℕ) else if a = (13860 : ℕ) then (0 : ℕ) else (truncated).
Uses library Finset.range, Finset.mem_range, Nat.mul_div_cancel.
Lean, lines 55–59
```
  have hmaps : ∀ x ∈ A.erase (A.max' hne), (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) (27720 * x / A.max' hne) ∈ Finset.range 10 := by
    intro x hx
    obtain ⟨a, ha, hax⟩ := forms x hx
    rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
    exact hS a ha
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 55–59 at 2de0bec6584f ↗
1. hmaps.s1 obtain printed form did not read back: shown as its Lean lines only
  obtain ⟨a, ha, hax⟩ := forms x hx
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 57 at 2de0bec6584f ↗
s11 obtain ∃ x ∈ A.erase (A.max' hne), ∃ y ∈ A.erase (A.max' hne), x ≠ y ∧ (fun (a : ℕ) => if a = (2520 : ℕ) then (2 : ℕ) else if a = (2772 : ℕ) then (7 : ℕ) else if a = (3080 : ℕ) then (6 : ℕ) else if a = (3465 : ℕ) then (9 : ℕ) else if a = (3960 : ℕ) then (8 : ℕ) else if a = (4620 : ℕ) then (5 : ℕ) else if a = (5040 : ℕ) then (5 : ℕ) else if a = (5544 : ℕ) then (4 : ℕ) else if a = (6160 : ℕ) then (7 : ℕ) else if a = (6930 : ℕ) then (3 : ℕ) else if a = (7560 : ℕ) then (3 : ℕ) else if a = (7920 : ℕ) then (9 : ℕ) else if a = (8316 : ℕ) then (2 : ℕ) else if a = (9240 : ℕ) then (1 : ℕ) else if a = (10080 : ℕ) then (1 : ℕ) else if a = (10395 : ℕ) then (6 : ℕ) else if a = (11088 : ℕ) then (6 : ℕ) else if a = (11880 : ℕ) then (7 : ℕ) else if a = (12320 : ℕ) then (4 : ℕ) else if a = (12600 : ℕ) then (4 : (truncated)
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, hc : (fun (a : ℕ) => if a = (2520 : ℕ) then (2 : ℕ) else if a = (2772 : ℕ) then (7 : ℕ) else if a = (3080 : ℕ) then (6 : ℕ) else if a = (3465 : ℕ) then (9 : ℕ) else if a = (3960 : ℕ) then (8 : ℕ) else if a = (4620 : ℕ) then (5 : ℕ) else if a = (5040 : ℕ) then (5 : ℕ) else if a = (5544 : ℕ) then (4 : ℕ) else if a = (6160 : ℕ) then (7 : ℕ) else if a = (6930 : ℕ) then (3 : ℕ) else if a = (7560 : ℕ) then (3 : ℕ) else if a = (7920 : ℕ) then (9 : ℕ) else if a = (8316 : ℕ) then (2 : ℕ) else if a = (9240 : ℕ) then (1 : ℕ) else if a = (10080 : ℕ) then (1 : ℕ) else if a = (10395 : ℕ) then (6 : ℕ) else if a = (11088 : ℕ) then (6 : ℕ) else if a = (11880 : ℕ) then (7 : ℕ) else if a = (12320 : ℕ) then (4 : ℕ) else if a = (12600 : ℕ) then (4 : ℕ) else if a = (13860 : ℕ) then (0 : ℕ) else if a = (15120 : ℕ) then (0 : ℕ) e (truncated).
Uses library Finset.exists_ne_map_eq_of_card_lt_of_maps_to, Finset.card_range.
Lean, lines 60–61
```
  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-11152e83/Proof.lean, lines 60–61 at 2de0bec6584f ↗
s12 obtain printed form did not read back: shown as its Lean lines only
```
  obtain ⟨a, ha, hax⟩ := forms x hx
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 62 at 2de0bec6584f ↗
s13 obtain printed form did not read back: shown as its Lean lines only
```
  obtain ⟨b, hb, hby⟩ := forms y hy
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 63 at 2de0bec6584f ↗
hab have a ≠ b
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hab : a ≠ b.
Lean, lines 65–69
```
  have hab : a ≠ b := by
    intro h
    subst h
    apply hxy
    omega
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 65–69 at 2de0bec6584f ↗

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

  have hpair : ∀ a ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), ∀ b ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), a ≠ b → (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) a = (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) b →
      12 * a.gcd b ≤ a ∨ 12 * a.gcd b ≤ b := by decide

targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 70–71 at 2de0bec6584f ↗

hgcd have a.gcd b * A.max' hne = (27720 : ℕ) * x.gcd y
Leaves ∃ a ∈ A, ∃ b ∈ A, (↑(a.gcd b) : ℚ) ≤ (↑a : ℚ) / (↑A.card : ℚ), with hgcd : a.gcd b * A.max' hne = (27720 : ℕ) * x.gcd y.
Uses library Nat.gcd_mul_right.
Lean, lines 72–75
```
  have hgcd : a.gcd b * A.max' hne = 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-11152e83/Proof.lean, lines 72–75 at 2de0bec6584f ↗
1. hgcd.h1 have ((27720 : ℕ) * x).gcd ((27720 : ℕ) * y) = (27720 : ℕ) * x.gcd y
  Leaves a.gcd b * A.max' hne = (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 73
  have h1 : Nat.gcd (27720 * x) (27720 * y) = 27720 * x.gcd y := Nat.gcd_mul_left 27720 x y
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 73 at 2de0bec6584f ↗
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 76
```
  have hxA := (Finset.mem_erase.mp hx).2
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 76 at 2de0bec6584f ↗
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 77
```
  have hyA := (Finset.mem_erase.mp hy).2
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 77 at 2de0bec6584f ↗
s19 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 79–83
```
  · refine ⟨x, hxA, y, hyA, key x y ?_⟩
    rw [hn]
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    have h3 : x.gcd y * 12 * 27720 ≤ x * 27720 := by nlinarith
    exact Nat.le_of_mul_le_mul_right h3 (by norm_num)
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 79–83 at 2de0bec6584f ↗
1. s19.h2 have (12 : ℕ) * a.gcd b * A.max' hne ≤ a * A.max' hne
  Leaves x.gcd y * (12 : ℕ) ≤ x, with h2 : (12 : ℕ) * a.gcd b * A.max' hne ≤ a * A.max' hne.
  Uses library Nat.mul_le_mul_right.
  Lean, line 81
  have h2 := Nat.mul_le_mul_right (A.max' hne) h
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 81 at 2de0bec6584f ↗
2. s19.h3 have x.gcd y * (12 : ℕ) * (27720 : ℕ) ≤ x * (27720 : ℕ) routine: nlinarith
  Leaves x.gcd y * (12 : ℕ) ≤ x, with h3 : x.gcd y * (12 : ℕ) * (27720 : ℕ) ≤ x * (27720 : ℕ).
  Lean, line 82
  have h3 : x.gcd y * 12 * 27720 ≤ x * 27720 := by nlinarith
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 82 at 2de0bec6584f ↗
s20 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 84–88
```
  · refine ⟨y, hyA, x, hxA, key y x ?_⟩
    rw [hn, Nat.gcd_comm]
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    have h3 : x.gcd y * 12 * 27720 ≤ y * 27720 := by nlinarith
    exact Nat.le_of_mul_le_mul_right h3 (by norm_num)
```
targets/erdos-402/nodes/variant-11152e83/Proof.lean, lines 84–88 at 2de0bec6584f ↗
1. s20.h2 have (12 : ℕ) * a.gcd b * A.max' hne ≤ b * A.max' hne
  Leaves x.gcd y * (12 : ℕ) ≤ y, with h2 : (12 : ℕ) * a.gcd b * A.max' hne ≤ b * A.max' hne.
  Uses library Nat.mul_le_mul_right.
  Lean, line 86
  have h2 := Nat.mul_le_mul_right (A.max' hne) h
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 86 at 2de0bec6584f ↗
2. s20.h3 have x.gcd y * (12 : ℕ) * (27720 : ℕ) ≤ y * (27720 : ℕ) routine: nlinarith
  Leaves x.gcd y * (12 : ℕ) ≤ y, with h3 : x.gcd y * (12 : ℕ) * (27720 : ℕ) ≤ y * (27720 : ℕ).
  Lean, line 87
  have h3 : x.gcd y * 12 * 27720 ≤ y * 27720 := by nlinarith
  targets/erdos-402/nodes/variant-11152e83/Proof.lean, line 87 at 2de0bec6584f ↗

The proof in Lean (Proof.lean)

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

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-11152e83/Proof.lean, sha256 1ea3a3f57a9a.

import Mathlib
import Nodes.«variant-11152e83».Context

/-! Graham's gcd conjecture (Erdős problem 402) for twelve-element sets. With M the largest
element, if gcd(M, x) > M/12 for every x then every other x is (j/k)M with j < k ≤ 11, so
L·x/M (L = lcm(1..11) = 27720) lies in a fixed set S of 41 values. S splits into 10 classes in
each of which any two distinct values c, d have 12·gcd(c, d) ≤ c or ≤ d; by pigeonhole two of
the 11 other elements share a class, and gcd(x, y)·L = gcd(c, d)·M transfers the bound. -/

theorem Opn.erdos_402_card_twelve :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 12 → ∃ 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
  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 * 12 ≤ A.max' hne
  · obtain ⟨x, hx, h⟩ := hw
    exact ⟨_, hM, x, hx, key _ x (by rw [hn]; exact h)⟩
  push_neg at hw
  have forms : ∀ x ∈ A.erase (A.max' hne), ∃ a ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), 27720 * x = a * A.max' hne := 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 < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hx.2) hx.1
    have hg := hw x hx.2
    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 hkN : k < 12 := by
      by_contra hh
      push_neg at hh
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh
      omega
    have hjk : j < k := by
      by_contra hh
      push_neg at hh
      have := Nat.mul_le_mul_left ((A.max' hne).gcd x) hh
      omega
    have hj1 : 1 ≤ j := by
      rcases Nat.eq_zero_or_pos j with h | h
      · subst h
        omega
      · exact h
    refine ⟨27720 * j / k, ?_, ?_⟩
    · interval_cases k <;> interval_cases j <;> decide
    · interval_cases k <;> interval_cases j <;> omega
  have hcard : (A.erase (A.max' hne)).card = 11 := by
    rw [Finset.card_erase_of_mem hM, hn]
  have hS : ∀ a ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) a < 10 := by decide
  have hmaps : ∀ x ∈ A.erase (A.max' hne), (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) (27720 * x / A.max' hne) ∈ Finset.range 10 := by
    intro x hx
    obtain ⟨a, ha, hax⟩ := forms x hx
    rw [Finset.mem_range, hax, Nat.mul_div_cancel _ hMpos]
    exact hS a ha
  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
  rw [hax, hby, Nat.mul_div_cancel _ hMpos, Nat.mul_div_cancel _ hMpos] at hc
  have hab : a ≠ b := by
    intro h
    subst h
    apply hxy
    omega
  have hpair : ∀ a ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), ∀ b ∈ ({2520, 2772, 3080, 3465, 3960, 4620, 5040, 5544, 6160, 6930, 7560, 7920, 8316, 9240, 10080, 10395, 11088, 11880, 12320, 12600, 13860, 15120, 15400, 15840, 16632, 17325, 17640, 18480, 19404, 19800, 20160, 20790, 21560, 22176, 22680, 23100, 23760, 24255, 24640, 24948, 25200} : Finset ℕ), a ≠ b → (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) a = (fun a : ℕ => if a = 2520 then 2 else if a = 2772 then 7 else if a = 3080 then 6 else if a = 3465 then 9 else if a = 3960 then 8 else if a = 4620 then 5 else if a = 5040 then 5 else if a = 5544 then 4 else if a = 6160 then 7 else if a = 6930 then 3 else if a = 7560 then 3 else if a = 7920 then 9 else if a = 8316 then 2 else if a = 9240 then 1 else if a = 10080 then 1 else if a = 10395 then 6 else if a = 11088 then 6 else if a = 11880 then 7 else if a = 12320 then 4 else if a = 12600 then 4 else if a = 13860 then 0 else if a = 15120 then 0 else if a = 15400 then 3 else if a = 15840 then 5 else if a = 16632 then 5 else if a = 17325 then 1 else if a = 17640 then 6 else if a = 18480 then 2 else if a = 19404 then 1 else if a = 19800 then 2 else if a = 20160 then 7 else if a = 20790 then 4 else if a = 21560 then 0 else if a = 22176 then 3 else if a = 22680 then 8 else if a = 23100 then 6 else if a = 23760 then 1 else if a = 24255 then 2 else if a = 24640 then 5 else if a = 24948 then 9 else if a = 25200 then 9 else 0) b →
      12 * a.gcd b ≤ a ∨ 12 * a.gcd b ≤ b := by decide
  have hgcd : a.gcd b * A.max' hne = 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 hpair a ha b hb hab hc with h | h
  · refine ⟨x, hxA, y, hyA, key x y ?_⟩
    rw [hn]
    have h2 := Nat.mul_le_mul_right (A.max' hne) h
    have h3 : x.gcd y * 12 * 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 (A.max' hne) h
    have h3 : x.gcd y * 12 * 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-11152e83».Context

/-! Graham's gcd conjecture (Erdős problem 402) for twelve-element sets. With M the largest
element, if gcd(M, x) > M/12 for every x then every other x is (j/k)M with j < k ≤ 11, so
L·x/M (L = lcm(1..11) = 27720) lies in a fixed set S of 41 values. S splits into 10 classes in
each of which any two distinct values c, d have 12·gcd(c, d) ≤ c or ≤ d; by pigeonhole two of
the 11 other elements share a class, and gcd(x, y)·L = gcd(c, d)·M transfers the bound. -/

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

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

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

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000299.json, merge commit 2de0bec6584f.

Verdict pass, from attestations/000299.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/000299.json, merge commit 2de0bec6584f.

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

import Mathlib

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 12 := ⟨Finset.Icc 1 12, 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-11152e83/Relation.lean, sha256 2c4d86d0fd5e.

-- 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 = 12 → ∃ 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 = 12 is a hypothesis, so the rational division is by 12; the same division appears in the root statement.

How to read this page

How to read a statement’s page →