Open Proof Network

Problems / erdos-402 / variant-d865c9c6

Graham's bound for |A| = 2

variant-d865c9c6

proved

A partial route to the problem.

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

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

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000145.json, merge commit 64f963463674.

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. s1 obtain printed form did not read back: shown as its Lean lines only
      obtain ⟨x, y, hxy, rfl⟩ := Finset.card_eq_two.mp hc

    targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 10 at 64f963463674 ↗

  2. hx0 have printed form did not read back: shown as its Lean lines only
      have hx0 : x ≠ 0 := by
    intro h; apply hA; simp [h]

    targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, lines 11–12 at 64f963463674 ↗

  3. hy0 have printed form did not read back: shown as its Lean lines only
      have hy0 : y ≠ 0 := by
    intro h; apply hA; simp [h]

    targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, lines 13–14 at 64f963463674 ↗

  4. key have printed form did not read back: shown as its Lean lines only
      have key : ∀ p q : ℕ, p ≠ 0 → q ≠ 0 → p < q → ((q.gcd p : ℕ) : ℚ) ≤ (q : ℚ) / 2 := by
    intro p q hp hq hpq
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left q p
    have hgle : q.gcd p ≤ p := Nat.le_of_dvd (Nat.pos_of_ne_zero hp) (Nat.gcd_dvd_right q p)
    have hk2 : 2 ≤ k := by
      by_contra hlt
      push_neg at hlt
      interval_cases k
      · exact hq (by rw [hk, mul_zero])
      · rw [mul_one] at hk
        omega
    have h2 : 2 * q.gcd p ≤ q := by
      calc 2 * q.gcd p = q.gcd p * 2 := by ring
        _ ≤ q.gcd p * k := Nat.mul_le_mul_left _ hk2
        _ = q := hk.symm
    rw [le_div_iff₀ (by norm_num : (0:ℚ) < 2)]
    have : ((2 * q.gcd p : ℕ) : ℚ) ≤ (q : ℚ) := by exact_mod_cast h2
    push_cast at this
    linarith

    targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, lines 15–33 at 64f963463674 ↗

    1. key.s1 obtain q.gcd p ∣ q

      Leaves (↑(q.gcd p) : ℚ) ≤ (↑q : ℚ) / (2 : ℚ), with k : ℕ, hk : q = q.gcd p * k.

      Uses library Nat.gcd_dvd_left.

      Lean, line 17
          obtain ⟨k, hk⟩ := Nat.gcd_dvd_left q p

      targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 17 at 64f963463674 ↗

    2. key.hgle have q.gcd p ≤ p

      Leaves (↑(q.gcd p) : ℚ) ≤ (↑q : ℚ) / (2 : ℚ), with hgle : q.gcd p ≤ p.

      Uses library Nat.le_of_dvd, Nat.pos_of_ne_zero, Nat.gcd_dvd_right.

      Lean, line 18
          have hgle : q.gcd p ≤ p := Nat.le_of_dvd (Nat.pos_of_ne_zero hp) (Nat.gcd_dvd_right q p)

      targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 18 at 64f963463674 ↗

    3. key.hk2 have (2 : ℕ) ≤ k

      Leaves (↑(q.gcd p) : ℚ) ≤ (↑q : ℚ) / (2 : ℚ), with hk2 : (2 : ℕ) ≤ k.

      Lean, lines 19–25
          have hk2 : 2 ≤ k := by
      by_contra hlt
      push_neg at hlt
      interval_cases k
      · exact hq (by rw [hk, mul_zero])
      · rw [mul_one] at hk
        omega

      targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, lines 19–25 at 64f963463674 ↗

      1. key.hk2.s1 case

        Leaves False.

        Uses library MulZeroClass.mul_zero Zero is a right absorbing element for multiplication .

        Lean, line 23
              · exact hq (by rw [hk, mul_zero])

        targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 23 at 64f963463674 ↗

      2. key.hk2.s2 case

        Leaves False.

        Uses library mul_one.

        Lean, lines 24–25
              · rw [mul_one] at hk
        omega

        targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, lines 24–25 at 64f963463674 ↗

    4. key.h2 have (2 : ℕ) * q.gcd p ≤ q

      Leaves (↑(q.gcd p) : ℚ) ≤ (↑q : ℚ) / (2 : ℚ), with h2 : (2 : ℕ) * q.gcd p ≤ q.

      Lean, lines 26–29
          have h2 : 2 * q.gcd p ≤ q := by
      calc 2 * q.gcd p = q.gcd p * 2 := by ring
        _ ≤ q.gcd p * k := Nat.mul_le_mul_left _ hk2
        _ = q := hk.symm

      targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, lines 26–29 at 64f963463674 ↗

      1. key.h2.s1 calc (2 : ℕ) * q.gcd p = q.gcd p * (2 : ℕ) routine: ring

        Closes the goal.

        Lean, line 27
              calc 2 * q.gcd p = q.gcd p * 2 := by ring

        targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 27 at 64f963463674 ↗

      2. key.h2.s2 calc q.gcd p * (2 : ℕ) ≤ q.gcd p * k

        Closes the goal.

        Uses library Nat.mul_le_mul_left.

        Lean, line 28
                _ ≤ q.gcd p * k := Nat.mul_le_mul_left _ hk2

        targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 28 at 64f963463674 ↗

      3. key.h2.s3 calc q.gcd p * k = q

        Closes the goal.

        Lean, line 29
                _ = q := hk.symm

        targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 29 at 64f963463674 ↗

    5. key.this have (↑((2 : ℕ) * q.gcd p) : ℚ) ≤ (↑q : ℚ)

      Leaves (↑(q.gcd p) : ℚ) * (2 : ℚ) ≤ (↑q : ℚ), with this : (↑((2 : ℕ) * q.gcd p) : ℚ) ≤ (↑q : ℚ).

      Lean, line 31
          have : ((2 * q.gcd p : ℕ) : ℚ) ≤ (q : ℚ) := by exact_mod_cast h2

      targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 31 at 64f963463674 ↗

  5. s5 case printed form did not read back: shown as its Lean lines only
      · exact ⟨y, by simp, x, by simp, by exact_mod_cast key x y hx0 hy0 h⟩

    targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 36 at 64f963463674 ↗

  6. s6 case printed form did not read back: shown as its Lean lines only
      · exact ⟨x, by simp, y, by simp, by exact_mod_cast key y x hy0 hx0 h⟩

    targets/erdos-402/nodes/variant-d865c9c6/Proof.lean, line 37 at 64f963463674 ↗

The proof in Lean (Proof.lean)

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

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

/-! Graham's gcd conjecture (Erdős problem 402) for two-element sets: the larger element's
gcd with the smaller is a proper divisor of it, so it is at most half of it. -/

theorem Opn.erdos_402_card_two :
    ∀ (A : Finset ℕ), 0 ∉ A → A.card = 2 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  intro A hA hc
  obtain ⟨x, y, hxy, rfl⟩ := Finset.card_eq_two.mp hc
  have hx0 : x ≠ 0 := by
    intro h; apply hA; simp [h]
  have hy0 : y ≠ 0 := by
    intro h; apply hA; simp [h]
  have key : ∀ p q : ℕ, p ≠ 0 → q ≠ 0 → p < q → ((q.gcd p : ℕ) : ℚ) ≤ (q : ℚ) / 2 := by
    intro p q hp hq hpq
    obtain ⟨k, hk⟩ := Nat.gcd_dvd_left q p
    have hgle : q.gcd p ≤ p := Nat.le_of_dvd (Nat.pos_of_ne_zero hp) (Nat.gcd_dvd_right q p)
    have hk2 : 2 ≤ k := by
      by_contra hlt
      push_neg at hlt
      interval_cases k
      · exact hq (by rw [hk, mul_zero])
      · rw [mul_one] at hk
        omega
    have h2 : 2 * q.gcd p ≤ q := by
      calc 2 * q.gcd p = q.gcd p * 2 := by ring
        _ ≤ q.gcd p * k := Nat.mul_le_mul_left _ hk2
        _ = q := hk.symm
    rw [le_div_iff₀ (by norm_num : (0:ℚ) < 2)]
    have : ((2 * q.gcd p : ℕ) : ℚ) ≤ (q : ℚ) := by exact_mod_cast h2
    push_cast at this
    linarith
  rw [hc]
  rcases lt_or_gt_of_ne hxy with h | h
  · exact ⟨y, by simp, x, by simp, by exact_mod_cast key x y hx0 hy0 h⟩
  · exact ⟨x, by simp, y, by simp, by exact_mod_cast key y x hy0 hx0 h⟩

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

/-! Graham's gcd conjecture (Erdős problem 402) for two-element sets: the larger element's
gcd with the smaller is a proper divisor of it, so it is at most half of it. -/

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

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

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

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000145.json, merge commit 64f963463674.

Verdict pass, from attestations/000145.json.

Submitter
tester-402-e514
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/000145.json, merge commit 64f963463674.

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

theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 2 :=
  ⟨{1, 2}, 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-d865c9c6/Relation.lean, sha256 a4f9ca76b459.
-- 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 = 2 → ∃ 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 = 2 is a hypothesis, so the rational division is by 2.

How to read this page

How to read a statement’s page →