The largest element coprime to some element

variant-950630b9

proved

A partial route to the problem.

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

For a finite set A of positive integers in which some maximal element m is coprime to some element b, there are a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

unverified · history

Lean

theorem Opn.erdos_402_max_coprime :
    ∀ (A : Finset ℕ), 0 ∉ A → (∃ m ∈ A, ∃ b ∈ A, (∀ c ∈ A, c ≤ m) ∧ m.Coprime b) →
      ∃ 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, 000170, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000170.json, merge commit 03eba3569164.

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.

hsub have A ⊆ Finset.Icc (1 : ℕ) m
Leaves (↑(m.gcd b) : ℚ) ≤ (↑m : ℚ) / (↑A.card : ℚ), with hsub : A ⊆ Finset.Icc (1 : ℕ) m.
Uses library Finset.Icc, Finset.mem_Icc, And.intro, Nat.pos_of_ne_zero.
Lean, lines 13–18
```
  have hsub : A ⊆ Finset.Icc 1 m := by
    intro c hc
    rw [Finset.mem_Icc]
    refine ⟨Nat.pos_of_ne_zero ?_, hmax c hc⟩
    rintro rfl
    exact hA hc
```
targets/erdos-402/nodes/variant-950630b9/Proof.lean, lines 13–18 at 03eba3569164 ↗
hcard have A.card ≤ m
Leaves (↑(m.gcd b) : ℚ) ≤ (↑m : ℚ) / (↑A.card : ℚ), with hcard : A.card ≤ m.
Lean, lines 19–21
```
  have hcard : A.card ≤ m := by
    have := Finset.card_le_card hsub
    simpa using this
```
targets/erdos-402/nodes/variant-950630b9/Proof.lean, lines 19–21 at 03eba3569164 ↗
1. hcard.this have A.card ≤ (Finset.Icc (1 : ℕ) m).card
  Leaves A.card ≤ m, with this : A.card ≤ (Finset.Icc (1 : ℕ) m).card.
  Uses library Finset.card_le_card.
  Lean, line 20
  have := Finset.card_le_card hsub
  targets/erdos-402/nodes/variant-950630b9/Proof.lean, line 20 at 03eba3569164 ↗
hpos have (0 : ℕ) < A.card
Leaves (↑(m.gcd b) : ℚ) ≤ (↑m : ℚ) / (↑A.card : ℚ), with hpos : (0 : ℕ) < A.card.
Uses library Finset.card_pos, Exists.intro.
Lean, line 22
```
  have hpos : 0 < A.card := Finset.card_pos.mpr ⟨m, hm⟩
```
targets/erdos-402/nodes/variant-950630b9/Proof.lean, line 22 at 03eba3569164 ↗

The proof in Lean (Proof.lean)

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

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-950630b9/Proof.lean, sha256 4885006a4fcf.

import Mathlib
import Nodes.«variant-950630b9».Context

/-! Graham's gcd conjecture (Erdős problem 402) when the largest element of `A` is coprime
to some element of `A`: then that pair has gcd 1, and `|A| ≤ max A` because `A` is a set of
positive integers at most `max A`. -/

theorem Opn.erdos_402_max_coprime :
    ∀ (A : Finset ℕ), 0 ∉ A → (∃ m ∈ A, ∃ b ∈ A, (∀ c ∈ A, c ≤ m) ∧ m.Coprime b) →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
  rintro A hA ⟨m, hm, b, hb, hmax, hcop⟩
  refine ⟨m, hm, b, hb, ?_⟩
  have hsub : A ⊆ Finset.Icc 1 m := by
    intro c hc
    rw [Finset.mem_Icc]
    refine ⟨Nat.pos_of_ne_zero ?_, hmax c hc⟩
    rintro rfl
    exact hA hc
  have hcard : A.card ≤ m := by
    have := Finset.card_le_card hsub
    simpa using this
  have hpos : 0 < A.card := Finset.card_pos.mpr ⟨m, hm⟩
  rw [Nat.Coprime] at hcop
  rw [hcop, le_div_iff₀ (by exact_mod_cast hpos)]
  simp only [Nat.cast_one, one_mul]
  exact_mod_cast hcard

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-950630b9».Context

/-! Graham's gcd conjecture (Erdős problem 402) when the largest element of `A` is coprime
to some element of `A`: then that pair has gcd 1, and `|A| ≤ max A` because `A` is a set of
positive integers at most `max A`. -/

theorem Opn.erdos_402_max_coprime :
    ∀ (A : Finset ℕ), 0 ∉ A → (∃ m ∈ A, ∃ b ∈ A, (∀ c ∈ A, c ≤ m) ∧ m.Coprime b) →
      ∃ 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

For a finite set A of positive integers in which some maximal element m is coprime to some element b, there are a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.

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

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

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000170.json, merge commit 03eba3569164.

Verdict pass, from attestations/000170.json.

Submitter: t0923-402-c
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/000170.json, merge commit 03eba3569164.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/variant-950630b9/Witness.lean, sha256 3acb84e54275.

import Mathlib

theorem witness : ∃ (A : Finset ℕ), 0 ∉ A ∧ ∃ m ∈ A, ∃ b ∈ A, (∀ c ∈ A, c ≤ m) ∧ m.Coprime b :=
  ⟨{1}, by decide, 1, by simp, 1, by simp, by simp, by norm_num⟩

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-950630b9/Relation.lean, sha256 87d12534f478.

-- 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 → (∃ m ∈ A, ∃ b ∈ A, (∀ c ∈ A, c ≤ m) ∧ m.Coprime b) →
      ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) := by
  rintro h A hA ⟨m, hm, -⟩
  obtain ⟨a, ha, b, hb, hab⟩ := h A hA ⟨m, hm⟩
  exact ⟨a, ha, b, hb, hab⟩

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

The hypothesis gives m ∈ A, so A is nonempty and A.card > 0; the rational division is never by zero.

How to read this page

How to read a statement’s page →