Problems / erdos-402 / variant-29101bbc
Graham's bound for |A| = 25
variant-29101bbc
proved
A partial route to the problem.
$\displaystyle \forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = 25 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$
Every set A of exactly twenty-five positive integers has a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.
Lean
theorem Opn.erdos_402_card_twenty_five :
∀ (A : Finset ℕ), 0 ∉ A → A.card = 25 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
sorryWhy 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, 000316, records the gate’s run.
The proof step by step (outline)
Checked by the kernel — an outline of the attested proof below: attestations/000316.json, merge commit 5af06fc66814.
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.
The proof in Lean (Proof.lean)
Checked by the kernel — these bytes are the ones its attestation names: attestations/000316.json, merge commit 5af06fc66814.
artifact_hash of the attestation below, so these are the bytes the gate checked. Rendered from targets/erdos-402/nodes/variant-29101bbc/Proof.lean, sha256 7bb9a0002fad.import Mathlib
import Nodes.«variant-29101bbc».Context
/-! Graham's gcd conjecture (Erdős problem 402) for twenty-five-element sets, closed by the
reduction `Opn.erdos_402_card_of_colouring` (declared dependency): with L = lcm(1..24),
the 179 values L·j/k (1 ≤ j < k < 25) split into 23 classes in which any two distinct values a, b
have 25·gcd(a, b) ≤ max(a, b), so pigeonhole on the 24 elements below the maximum finishes. -/
theorem Opn.erdos_402_card_twenty_five :
∀ (A : Finset ℕ), 0 ∉ A → A.card = 25 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
intro A hA hn
exact Opn.erdos_402_card_of_colouring 25 5354228880 ([223092870, 232792560, 243374040, 254963280, 267711444, 281801520, 297457160, 314954640, 334639305, 356948592, 382444920, 411863760, 446185740, 465585120, 486748080, 509926560, 535422888, 563603040, 594914320, 629909280, 669278610, 698377680, 713897184, 730122120, 764889840, 803134332, 823727520, 845404560, 892371480, 931170240, 944863920, 973496160, 1003917915, 1019853120, 1070845776, 1115464350, 1127206080, 1147334760, 1163962800, 1189828640, 1216870200, 1235591280, 1259818560, 1274816400, 1338557220, 1396755360, 1409007600, 1427794368, 1460244240, 1487285800, 1529779680, 1561650090, 1574773200, 1606268664, 1629547920, 1647455040, 1673196525, 1690809120, 1703618280, 1784742960, 1862340480, 1873980108, 1889727840, 1912224600, 1946992320, 1972610640, 2007835830, 2039706240, 2059318800, 2082200120, 2095133040, 2141691552, 2190366360, 2204682480, 2230928700, 2254412160, 2294669520, 2327925600, 2342475135, 2379657280, 2409402996, 2433740400, 2454021570, 2471182560, 2498640144, 2519637120, 2536213680, 2549632800, 2560718160, 2677114440, 2793510720, 2804596080, 2818015200, 2834591760, 2855588736, 2883046320, 2900207310, 2920488480, 2944825884, 2974571600, 3011753745, 3026303280, 3059559360, 3099816720, 3123300180, 3149546400, 3163862520, 3212537328, 3259095840, 3272028760, 3294910080, 3314522640, 3346393050, 3381618240, 3407236560, 3442004280, 3464501040, 3480248772, 3491888400, 3569485920, 3650610600, 3663419760, 3681032355, 3706773840, 3724680960, 3747960216, 3779455680, 3792578790, 3824449200, 3866943080, 3893984640, 3926434512, 3945221280, 3957473520, 4015671660, 4079412480, 4094410320, 4118637600, 4137358680, 4164400240, 4190266080, 4206894120, 4227022800, 4238764530, 4283383104, 4334375760, 4350310965, 4380732720, 4409364960, 4423058640, 4461857400, 4508824320, 4530501360, 4551094548, 4589339040, 4624106760, 4640331696, 4655851200, 4684950270, 4724319600, 4759314560, 4790625840, 4818805992, 4844302320, 4867480800, 4888643760, 4908043140, 4942365120, 4971783960, 4997280288, 5019589575, 5039274240, 5056771720, 5072427360, 5086517436, 5099265600, 5110854840, 5121436320, 5131136010] : List ℕ).toFinset
(fun a : ℕ => ((([(223092870, 14), (232792560, 19), (243374040, 21), (254963280, 9), (267711444, 20), (281801520, 3), (297457160, 12), (314954640, 22), (334639305, 17), (356948592, 16), (382444920, 15), (411863760, 18), (446185740, 11), (465585120, 20), (486748080, 5), (509926560, 17), (535422888, 13), (563603040, 21), (594914320, 8), (629909280, 16), (669278610, 6), (698377680, 17), (713897184, 18), (730122120, 16), (764889840, 10), (803134332, 12), (823727520, 19), (845404560, 18), (892371480, 4), (931170240, 11), (944863920, 19), (973496160, 14), (1003917915, 9), (1019853120, 5), (1070845776, 7), (1115464350, 10), (1127206080, 17), (1147334760, 3), (1163962800, 15), (1189828640, 15), (1216870200, 9), (1235591280, 20), (1259818560, 18), (1274816400, 6), (1338557220, 2), (1396755360, 10), (1409007600, 5), (1427794368, 6), (1460244240, 15), (1487285800, 17), (1529779680, 12), (1561650090, 13), (1574773200, 13), (1606268664, 14), (1629547920, 4), (1647455040, 13), (1673196525, 3), (1690809120, 16), (1703618280, 8), (1784742960, 1), (1862340480, 13), (1873980108, 3), (1889727840, 6), (1912224600, 11), (1946992320, 19), (1972610640, 12), (2007835830, 8), (2039706240, 7), (2059318800, 14), (2082200120, 6), (2095133040, 7), (2141691552, 9), (2190366360, 1), (2204682480, 14), (2230928700, 7), (2254412160, 4), (2294669520, 13), (2327925600, 5), (2342475135, 18), (2379657280, 10), (2409402996, 17), (2433740400, 4), (2454021570, 15), (2471182560, 17), (2498640144, 5), (2519637120, 12), (2536213680, 9), (2549632800, 2), (2560718160, 6), (2677114440, 0), (2793510720, 2), (2804596080, 14), (2818015200, 6), (2834591760, 2), (2855588736, 2), (2883046320, 11), (2900207310, 21), (2920488480, 7), (2944825884, 4), (2974571600, 16), (3011753745, 10), (3026303280, 0), (3059559360, 16), (3099816720, 2), (3123300180, 9), (3149546400, 9), (3163862520, 18), (3212537328, 11), (3259095840, 8), (3272028760, 5), (3294910080, 5), (3314522640, 11), (3346393050, 12), (3381618240, 10), (3407236560, 2), (3442004280, 6), (3464501040, 3), (3480248772, 6), (3491888400, 1), (3569485920, 3), (3650610600, 10), (3663419760, 8), (3681032355, 1), (3706773840, 4), (3724680960, 9), (3747960216, 10), (3779455680, 1), (3792578790, 17), (3824449200, 8), (3866943080, 2), (3893984640, 6), (3926434512, 12), (3945221280, 11), (3957473520, 3), (4015671660, 5), (4079412480, 0), (4094410320, 4), (4118637600, 1), (4137358680, 11), (4164400240, 7), (4190266080, 12), (4206894120, 7), (4227022800, 7), (4238764530, 18), (4283383104, 8), (4334375760, 18), (4350310965, 7), (4380732720, 3), (4409364960, 5), (4423058640, 14), (4461857400, 19), (4508824320, 1), (4530501360, 8), (4551094548, 15), (4589339040, 4), (4624106760, 17), (4640331696, 10), (4655851200, 16), (4684950270, 16), (4724319600, 0), (4759314560, 11), (4790625840, 0), (4818805992, 16), (4844302320, 19), (4867480800, 13), (4888643760, 18), (4908043140, 20), (4942365120, 6), (4971783960, 1), (4997280288, 0), (5019589575, 4), (5039274240, 7), (5056771720, 9), (5072427360, 13), (5086517436, 1), (5099265600, 15), (5110854840, 12), (5121436320, 21), (5131136010, 22)] : List (ℕ × ℕ)).lookup a).getD 0))
(by norm_num) (by norm_num) (by decide +kernel) (by decide +kernel) (by decide +kernel) A hA hnWhat 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).
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-29101bbc».Context
/-! Graham's gcd conjecture (Erdős problem 402) for twenty-five-element sets, closed by the
reduction `Opn.erdos_402_card_of_colouring` (declared dependency): with L = lcm(1..24),
the 179 values L·j/k (1 ≤ j < k < 25) split into 23 classes in which any two distinct values a, b
have 25·gcd(a, b) ≤ max(a, b), so pigeonhole on the 24 elements below the maximum finishes. -/
theorem Opn.erdos_402_card_twenty_five :
∀ (A : Finset ℕ), 0 ∉ A → A.card = 25 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ) := by
sorryA 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| = 25 \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}$
Every set A of exactly twenty-five positive integers has a, b ∈ A (possibly equal) with gcd(a, b) ≤ a/|A|. The division is in ℚ.
Rendered from gloss/13b95e99dcc9….md · Improve these words →
Rendered from targets/erdos-402/nodes/variant-29101bbc/Statement.lean. Origin: variant (partial).
Depends on (1), each in words
Depends on, each in words where someone has written them:
- spec-fa8046e4
Opn.erdos_402_card_of_colouring: $\begin{aligned}&n \ge 2,\ L > 0,\ S \subset \mathbb{N}\ \text{finite},\ c : \mathbb{N} \to \mathbb{N},\\&\forall k < n,\ \forall j < k,\ j > 0:\ k \mid L j\ \wedge\ L j / k \in S,\qquad \forall a \in S:\ c(a) + 2 < n,\\&\forall a, b \in S,\ a \ne b,\ c(a) = c(b):\ n \cdot \gcd(a,b) \le a\ \vee\ n \cdot \gcd(a,b) \le b\\&\Longrightarrow\ \forall A \subset \mathbb{N}\ \text{finite}:\ 0 \notin A,\ |A| = n \Rightarrow \exists\, a, b \in A:\ \gcd(a,b) \le \frac{a}{|A|}\end{aligned}$ · used by the proof
Attestation: pass, 7 of 7 checks
Checked by the kernel — the gate’s record of the run: attestations/000316.json, merge commit 5af06fc66814.
Verdict pass, from attestations/000316.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/000316.json, merge commit 5af06fc66814.
d1a545e2b790.import Mathlib import Nodes.«variant-29101bbc».Context theorem witness : ∃ A : Finset ℕ, 0 ∉ A ∧ A.card = 25 := ⟨Finset.Icc 1 25, 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.
b95bd9d1cf6a.-- relation: partial
import Mathlib
import Nodes.«variant-29101bbc».Context
theorem relation :
(∀ (A : Finset ℕ), 0 ∉ A → A.Nonempty → ∃ᵉ (a ∈ A) (b ∈ A), a.gcd b ≤ (a / A.card : ℚ)) →
(∀ (A : Finset ℕ), 0 ∉ A → A.card = 25 → ∃ a ∈ A, ∃ b ∈ A, a.gcd b ≤ (a / A.card : ℚ)) := by
intro h A h0 hc
exact h A h0 (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
The hypothesis A.card = 25 makes A.card positive, so the rational division is never by zero.