Open Proof Network

Problems / erdos-402 / spec-48bd0126

Max-fraction form of the elements below max A

spec-48bd0126 Opn.erdos_402_max_fraction_form

proved

Proposed by a contributor.

$\displaystyle \forall n \in \mathbb{N},\ \forall A \subset \mathbb{N}\ \text{finite}\ \text{nonempty},\ M = \max A:\ 0 \notin A,\ \bigl(\forall x \in A,\ M < \gcd(M, x) \cdot n\bigr) \Rightarrow \forall x \in A \setminus \{M\}\ \exists\, j, k \in \mathbb{N}:\ 1 \le j < k < n,\ k x = j M$

For a finite nonempty set A of positive integers with largest element M and any n ∈ ℕ: if M < n·gcd(M, x) for every x ∈ A, then every element other than M is (j/k)·M for some 1 ≤ j < k < n, written as the equation k·x = j·M over ℕ.

unverified · history

Lean
theorem Opn.erdos_402_max_fraction_form :
    ∀ (n : ℕ) (A : Finset ℕ) (hne : A.Nonempty), 0 ∉ A →
      (∀ x ∈ A, A.max' hne < (A.max' hne).gcd x * n) →
      ∀ x ∈ A.erase (A.max' hne), ∃ j k : ℕ, 1 ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne := 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, 000257, records the gate’s run.

The proof step by step (outline)

Checked by the kernel — an outline of the attested proof below: attestations/000257.json, merge commit 4ca089804e75.

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 x ≠ A.max' hne ∧ x ∈ A

    Leaves ∃ (j : ℕ) (k : ℕ), (1 : ℕ) ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne, with hxM : x ≠ A.max' hne, hxA : x ∈ A.

    Lean, line 16
      obtain ⟨hxM, hxA⟩ := hx

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 16 at 4ca089804e75 ↗

  2. hxpos have (0 : ℕ) < x

    Leaves ∃ (j : ℕ) (k : ℕ), (1 : ℕ) ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne, with hxpos : (0 : ℕ) < x.

    Uses library Nat.pos_of_ne_zero.

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

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 17 at 4ca089804e75 ↗

  3. hlt have x < A.max' hne

    Leaves ∃ (j : ℕ) (k : ℕ), (1 : ℕ) ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne, with hlt : x < A.max' hne.

    Uses library lt_of_le_of_ne, Finset.le_max'.

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

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 18 at 4ca089804e75 ↗

  4. hg have A.max' hne < (A.max' hne).gcd x * n

    Leaves ∃ (j : ℕ) (k : ℕ), (1 : ℕ) ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne, with hg : A.max' hne < (A.max' hne).gcd x * n.

    Lean, line 19
      have hg := hw x hxA

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 19 at 4ca089804e75 ↗

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

    Leaves ∃ (j : ℕ) (k : ℕ), (1 : ℕ) ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne, with hgpos : (0 : ℕ) < (A.max' hne).gcd x.

    Uses library Nat.gcd_pos_of_pos_right.

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

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 20 at 4ca089804e75 ↗

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

    Leaves ∃ (j : ℕ) (k : ℕ), (1 : ℕ) ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne, with k : ℕ, hk : A.max' hne = (A.max' hne).gcd x * k.

    Uses library Nat.gcd_dvd_left.

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

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 21 at 4ca089804e75 ↗

  7. s7 obtain (A.max' hne).gcd x ∣ x

    Leaves ∃ (j : ℕ) (k : ℕ), (1 : ℕ) ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne, with j : ℕ, hj : x = (A.max' hne).gcd x * j.

    Uses library Nat.gcd_dvd_right.

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

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 22 at 4ca089804e75 ↗

  8. s8 case

    Leaves (1 : ℕ) ≤ j.

    Uses library Nat.eq_zero_or_pos.

    Lean, lines 24–27
      · rcases Nat.eq_zero_or_pos j with h | h
    · rw [h, Nat.mul_zero] at hj
      omega
    · exact h

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, lines 24–27 at 4ca089804e75 ↗

    1. s8.s1 case

      Leaves (1 : ℕ) ≤ j.

      Uses library Nat.mul_zero.

      Lean, lines 25–26
          · rw [h, Nat.mul_zero] at hj
      omega

      targets/erdos-402/nodes/spec-48bd0126/Proof.lean, lines 25–26 at 4ca089804e75 ↗

    2. s8.s2 case

      Leaves (1 : ℕ) ≤ j.

      Lean, line 27
          · exact h

      targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 27 at 4ca089804e75 ↗

  9. s9 case

    Leaves j < k.

    Uses library Nat.lt_of_mul_lt_mul_left.

    Lean, lines 28–31
      · have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
      rw [← hj, ← hk]
      exact hlt
    exact Nat.lt_of_mul_lt_mul_left h1

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, lines 28–31 at 4ca089804e75 ↗

    1. s9.h1 have (A.max' hne).gcd x * j < (A.max' hne).gcd x * k

      Leaves j < k, with h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k.

      Lean, lines 28–30
        · have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
      rw [← hj, ← hk]
      exact hlt

      targets/erdos-402/nodes/spec-48bd0126/Proof.lean, lines 28–30 at 4ca089804e75 ↗

  10. s10 case

    Leaves k < n.

    Uses library Nat.lt_of_mul_lt_mul_left.

    Lean, lines 32–35
      · have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
      rw [← hk]
      exact hg
    exact Nat.lt_of_mul_lt_mul_left h1

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, lines 32–35 at 4ca089804e75 ↗

    1. s10.h1 have (A.max' hne).gcd x * k < (A.max' hne).gcd x * n

      Leaves k < n, with h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n.

      Lean, lines 32–34
        · have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
      rw [← hk]
      exact hg

      targets/erdos-402/nodes/spec-48bd0126/Proof.lean, lines 32–34 at 4ca089804e75 ↗

  11. s11 case

    Leaves k * x = j * A.max' hne.

    Lean, lines 36–38
      · calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
      _ = j * ((A.max' hne).gcd x * k) := by ring
      _ = j * A.max' hne := by rw [← hk]

    targets/erdos-402/nodes/spec-48bd0126/Proof.lean, lines 36–38 at 4ca089804e75 ↗

    1. s11.s1 calc k * x = k * ((A.max' hne).gcd x * j)

      Closes the goal.

      Lean, line 36
        · calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]

      targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 36 at 4ca089804e75 ↗

    2. s11.s2 calc routine: ring

      Closes the goal.

      Lean, line 37
            _ = j * ((A.max' hne).gcd x * k) := by ring

      targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 37 at 4ca089804e75 ↗

    3. s11.s3 calc

      Closes the goal.

      Lean, line 38
            _ = j * A.max' hne := by rw [← hk]

      targets/erdos-402/nodes/spec-48bd0126/Proof.lean, line 38 at 4ca089804e75 ↗

The proof in Lean (Proof.lean)

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

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/spec-48bd0126/Proof.lean, sha256 c8557978ef9e.
import Mathlib
import Nodes.«spec-48bd0126».Context

/-! The structure lemma every fixed-size case of Erdős problem 402 (Graham's gcd problem) repeats:
with M the largest element of A, if gcd(M, x) > M/n for every x in A, then every other element
of A is (j/k)·M with 1 ≤ j < k < n. A card-n variant needs it with n = A.card: when some x has
gcd(M, x) ≤ M/n the pair (M, x) already answers, and otherwise every element is one of finitely
many fractions of M, which a finite check finishes. -/

theorem Opn.erdos_402_max_fraction_form :
    ∀ (n : ℕ) (A : Finset ℕ) (hne : A.Nonempty), 0 ∉ A →
      (∀ x ∈ A, A.max' hne < (A.max' hne).gcd x * n) →
      ∀ x ∈ A.erase (A.max' hne), ∃ j k : ℕ, 1 ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne := by
  intro n A hne hA hw x hx
  rw [Finset.mem_erase] at hx
  obtain ⟨hxM, hxA⟩ := hx
  have hxpos : 0 < x := Nat.pos_of_ne_zero (fun h => hA (h ▸ hxA))
  have hlt : x < A.max' hne := lt_of_le_of_ne (Finset.le_max' A x hxA) hxM
  have hg := hw x hxA
  have hgpos : 0 < (A.max' hne).gcd x := Nat.gcd_pos_of_pos_right _ hxpos
  obtain ⟨k, hk⟩ := Nat.gcd_dvd_left (A.max' hne) x
  obtain ⟨j, hj⟩ := Nat.gcd_dvd_right (A.max' hne) x
  refine ⟨j, k, ?_, ?_, ?_, ?_⟩
  · rcases Nat.eq_zero_or_pos j with h | h
    · rw [h, Nat.mul_zero] at hj
      omega
    · exact h
  · have h1 : (A.max' hne).gcd x * j < (A.max' hne).gcd x * k := by
      rw [← hj, ← hk]
      exact hlt
    exact Nat.lt_of_mul_lt_mul_left h1
  · have h1 : (A.max' hne).gcd x * k < (A.max' hne).gcd x * n := by
      rw [← hk]
      exact hg
    exact Nat.lt_of_mul_lt_mul_left h1
  · calc k * x = k * ((A.max' hne).gcd x * j) := by rw [← hj]
      _ = j * ((A.max' hne).gcd x * k) := by ring
      _ = j * A.max' hne := by rw [← hk]

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.«spec-48bd0126».Context

/-! The structure lemma every fixed-size case of Erdős problem 402 (Graham's gcd problem) repeats:
with M the largest element of A, if gcd(M, x) > M/n for every x in A, then every other element
of A is (j/k)·M with 1 ≤ j < k < n. A card-n variant needs it with n = A.card: when some x has
gcd(M, x) ≤ M/n the pair (M, x) already answers, and otherwise every element is one of finitely
many fractions of M, which a finite check finishes. -/

theorem Opn.erdos_402_max_fraction_form :
    ∀ (n : ℕ) (A : Finset ℕ) (hne : A.Nonempty), 0 ∉ A →
      (∀ x ∈ A, A.max' hne < (A.max' hne).gcd x * n) →
      ∀ x ∈ A.erase (A.max' hne), ∃ j k : ℕ, 1 ≤ j ∧ j < k ∧ k < n ∧ k * x = j * A.max' hne := 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 n \in \mathbb{N},\ \forall A \subset \mathbb{N}\ \text{finite}\ \text{nonempty},\ M = \max A:\ 0 \notin A,\ \bigl(\forall x \in A,\ M < \gcd(M, x) \cdot n\bigr) \Rightarrow \forall x \in A \setminus \{M\}\ \exists\, j, k \in \mathbb{N}:\ 1 \le j < k < n,\ k x = j M$

For a finite nonempty set A of positive integers with largest element M and any n ∈ ℕ: if M < n·gcd(M, x) for every x ∈ A, then every element other than M is (j/k)·M for some 1 ≤ j < k < n, written as the equation k·x = j·M over ℕ.

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

Rendered from targets/erdos-402/nodes/spec-48bd0126/Statement.lean. Origin: authored.

Attestation: pass, 7 of 7 checks

Checked by the kernel — the gate’s record of the run: attestations/000257.json, merge commit 4ca089804e75.

Verdict pass, from attestations/000257.json.

Submitter
t0929-6
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/000257.json, merge commit 4ca089804e75.

Witness.lean — checked at step 7 of the run recorded below: pass. Rendered from targets/erdos-402/nodes/spec-48bd0126/Witness.lean, sha256 3d23336f74ec.
import Mathlib

theorem witness : ∃ (n : ℕ) (A : Finset ℕ) (hne : A.Nonempty) (x : ℕ),
    (0 : ℕ) ∉ A ∧ (∀ x ∈ A, A.max' hne < (A.max' hne).gcd x * n) ∧ x ∈ A.erase (A.max' hne) :=
  ⟨3, {1, 2}, ⟨1, by simp⟩, 1, by decide, 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 →

Acknowledged findings (1)

Untrusted contributor text — the prover’s justification for a finding.

Untrusted: acknowledgment of a off-by-one-range finding at 1 ≤ j

The conclusion says the numerator j is positive, which is intended: x is a positive element of A, so x = (j/k)·M forces j ≥ 1.

How to read this page

How to read a statement’s page →