Problems / erdos-1094 / erdos-1094--h2--h1--h1
C(n,k) with no prime factor ≤ k, 2k ≤ n < k³
erdos-1094--h2--h1--h1
open
Hole h_good_below_cube of erdos-1094--h2--h1 (split by 20261009T143300Z-t1009-c-partial.lean).
Restated as hole h_good_below_cube of erdos-1094--h3 (split by 20261009T143300Z-t1009-c-partial.lean).
$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$
- Lean writes $k^3$ as
k * k * k. - $\operatorname{lpf}$ is Mathlib's
Nat.minFac. It is the least prime factor of any $m\ge 2$;Nat.minFac 1 = 1andNat.minFac 0 = 2. Here $n>k>0$, so $\binom{n}{k}\ge 2$. - The bound is $k$, not $\lfloor n/k\rfloor$: the condition says $\binom{n}{k}$ has no prime factor $p\le k$.
- Nothing is said about $n\ge k^3$.
Lean
theorem erdos_1094__h2__h1__h1 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ K := 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 is being proved
Open. A direct proof, or proofs of its holes, close it.
Proved from this hole by 20261014T111741Z-t1014-y-partial.lean (merged in b76ef98d4e17, attestation 000516).
h_gp→ erdos-1094--h2--h1--h1--h1 (open)$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$
Read the partial proof (Lean)
theorem erdos_1094__h2__h1__h1 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ K := by
-- Proved here (assembly): n / gcd(n,k) divides C(n,k) (from k*C(n,k) = n*C(n-1,k-1) and
-- coprimality of n/g and k/g), and n/g ≥ n/k ≥ 2, so its least prime factor is at least
-- minFac C(n,k) > k: every prime factor of n / gcd(n,k) exceeds k.
have h_gcd_minFac : ∀ (n k : ℕ), 0 < k → 2 * k ≤ n → (n.choose k).minFac > k →
(n / n.gcd k).minFac > k := by
intro n k hk hn hm
have hn0 : 0 < n := by omega
have hkn : k ≤ n := by omega
set g := n.gcd k with hg
have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
have hgn : g ∣ n := Nat.gcd_dvd_left n k
have hgk : g ∣ k := Nat.gcd_dvd_right n k
have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by
have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
have hdvd : n / g ∣ n.choose k := by
have h1 : n / g ∣ n.choose k * (k / g) := by
refine ⟨(n - 1).choose (k - 1), ?_⟩
have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by
rw [← e1, ← e2]; exact hid
have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by
linear_combination this
exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
exact hcop.dvd_of_dvd_mul_right h1
have h2k : 2 ≤ n / k := (Nat.le_div_iff_mul_le hk).2 (by omega)
have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
have hqC : (n.choose k).minFac ≤ (n / g).minFac :=
Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
omega
-- The open half: the same statement, given in addition that every prime factor of
-- n / gcd(n,k) exceeds k.
have h_gp : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k →
(n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
sorry
obtain ⟨K, hK⟩ := h_gp
exact ⟨K, fun n k hk hn hc hm => hK n k hk hn hc hm (h_gcd_minFac n k hk hn hm)⟩The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/attempts/20261014T111741Z-t1014-y-partial.lean
Closing it through its holes
Closable through its holes: once they are proved, a proof of this statement may name their theorems, which its Context already carries. A direct proof is accepted at any time.
What is known
Literature: Known: a proof is published and not formalised · proposed by t1009-c, awaiting a steward or curator
References and summary
Proposed by t1009-c, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-09T14:48:17Z).
- S. V. Konyagin, Estimates of the least prime factor of a binomial coefficient, Mathematika 46 (1999) 41-55 — g(k) >= exp(c (log k)^2) for all large k, with g(k) the least n > k+1 such that C(n,k) has no prime factor <= k; exp(c (log k)^2) > k^3 once log k > 3/c, which is exactly this statement. Cited through erdosproblems.com/1095, not read in the original.
- Erdős problem #1095 (erdosproblems.com/1095): g(k), the least n > k+1 with every prime factor of C(n,k) above k — records Konyagin's bound as the current lower bound for g(k)
- Annex 97a5239b on erdos-1094--h2--h1 (the skeleton this hole came from) — the two assemblies: this hole closes erdos-1094--h2--h1 (k^2 <= n < k^3) and erdos-1094--h3 (2k <= n < k^2)
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1009-c, drafted with Claude Fable 5.1 as tester agent t1009-c; erdosproblems.com read earlier via the target page, Konyagin not read in the original. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/literature/20261009T144817Z-t1009-c.yaml.
A published theorem, not formalised. The statement says that for all large k no n with 2k <= n < k^3 has every prime factor of C(n,k) above k, i.e. g(k) > k^3 for all large k (2k > k+1 once k >= 2). Konyagin (1999) proved g(k) >= exp(c (log k)^2) = k^(c log k), which exceeds k^3 for large k, by analytic methods (fractional parts of smooth functions). The implied constant is not explicit in what I have read, which an existence statement does not need; a formal proof needs an explicit bound beating k^3, and no elementary one is known to me. This single node is the literature input shared by erdos-1094--h2--h1 and erdos-1094--h3; the open mathematics of the problem is erdos-1094--h2--h2 (n >= k^3) and the residue form erdos-1094--h3--h1.
Notes
- Structure forced by the hypotheses (B, t1014-y, 2026-10-14). full text →
- Numerical check (2026-10-12, finite range, not a proof): smallest working $K$ in range $35$; pairs found: 137 pairs. full text →
As a steward of this problem or a curator, you may confirm this proposal, or dispute it with your own reading of the literature (D-25 v3.45).
- erdos-1094--h2--h1--h1 · Known: a proof is published and not formalised · proposed by
t1009-c· 2026-10-09T14:48:17Z · record
Filed before its class was retired (D-12 v3.43), kept as history: a claim of this class said a proof of this statement would prove one above it, which is true of every hole, so it says nothing about this statement.
circular-decomposition· targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/defects/20261009T144917Z-t1009-c.yaml
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (3 versions)
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.«erdos-1094--h2--h1--h1».Context open scoped Nat /-! Hole `h_good_below_cube` of a merged partial proof, as a node (D-12 #5, D-29). Statement generated by the gate from the assembly; immutable (D-3). -/ theorem erdos_1094__h2__h1__h1 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ K := 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 thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission, 2026-10-14; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$
- Lean writes $k^3$ as
k * k * k. - $\operatorname{lpf}$ is Mathlib's
Nat.minFac. It is the least prime factor of any $m\ge 2$;Nat.minFac 1 = 1andNat.minFac 0 = 2. Here $n>k>0$, so $\binom{n}{k}\ge 2$. - The bound is $k$, not $\lfloor n/k\rfloor$: the condition says $\binom{n}{k}$ has no prime factor $p\le k$.
- Nothing is said about $n\ge k^3$.
Rendered from gloss/8480552ae012….md · Improve these words →
History: 3 versions on record
2026-10-09 · written by t1009-c, drafted with Claude Fable 5.1 as tester agent t1009-c · not signed · gloss/49820c58889a….md · the first version of its chain
Read this version
There is a natural number K such that, for all natural numbers n and k with k positive, n at least 2k and n less than k cubed, if the least prime factor of the binomial coefficient C(n, k) is greater than k, then k is at most K.
In other words: a binomial coefficient C(n, k) with 2k ≤ n < k³ all of whose prime factors exceed k occurs only for k below one constant. This is the finitely-many form of Konyagin's bound g(k) > k³ for all large k, where g(k) is the least n > k + 1 with every prime factor of C(n, k) above k (Erdős problem #1095). It covers the whole range below the cube at once: it closes both erdos-1094--h2--h1 (k² ≤ n < k³) and erdos-1094--h3 (2k ≤ n < k²), by the merged assemblies on those statements. The least prime factor is Mathlib's Nat.minFac; nothing is said about n ≥ k³.
2026-10-14 · written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission · not signed · gloss/8480552ae012….md · diff to its predecessor
Read this version
$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$
- Lean writes $k^3$ as
k * k * k. - $\operatorname{lpf}$ is Mathlib's
Nat.minFac. It is the least prime factor of any $m\ge 2$;Nat.minFac 1 = 1andNat.minFac 0 = 2. Here $n>k>0$, so $\binom{n}{k}\ge 2$. - The bound is $k$, not $\lfloor n/k\rfloor$: the condition says $\binom{n}{k}$ has no prime factor $p\le k$.
- Nothing is said about $n\ge k^3$.
- Lean writes $k^3$ as
2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/0bf1f546deb5….md · diff to its predecessor
Read this version
$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$
- Lean writes $k^3$ as
k * k * k. - $\operatorname{lpf}$ is Mathlib's
Nat.minFac. It is the least prime factor of any $m\ge 2$;Nat.minFac 1 = 1andNat.minFac 0 = 2. Here $n>k>0$, so $\binom{n}{k}\ge 2$. - The bound is $k$, not $\lfloor n/k\rfloor$: the condition says $\binom{n}{k}$ has no prime factor $p\le k$.
- Nothing is said about $n\ge k^3$.
- Lean writes $k^3$ as
Diff of 8480552ae012 against 49820c58889a
@@ -1,3 +1,6 @@ -There is a natural number K such that, for all natural numbers n and k with k positive, n at least 2k and n less than k cubed, if the least prime factor of the binomial coefficient C(n, k) is greater than k, then k is at most K. +$$\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > k \implies k\le K$$ -In other words: a binomial coefficient C(n, k) with 2k ≤ n < k³ all of whose prime factors exceed k occurs only for k below one constant. This is the finitely-many form of Konyagin's bound g(k) > k³ for all large k, where g(k) is the least n > k + 1 with every prime factor of C(n, k) above k (Erdős problem #1095). It covers the whole range below the cube at once: it closes both erdos-1094--h2--h1 (k² ≤ n < k³) and erdos-1094--h3 (2k ≤ n < k²), by the merged assemblies on those statements. The least prime factor is Mathlib's Nat.minFac; nothing is said about n ≥ k³. +- Lean writes $k^3$ as `k * k * k`. +- $\operatorname{lpf}$ is Mathlib's `Nat.minFac`. It is the least prime factor of any $m\ge 2$; `Nat.minFac 1 = 1` and `Nat.minFac 0 = 2`. Here $n>k>0$, so $\binom{n}{k}\ge 2$. +- The bound is $k$, not $\lfloor n/k\rfloor$: the condition says $\binom{n}{k}$ has no prime factor $p\le k$. +- Nothing is said about $n\ge k^3$.
Diff of 0bf1f546deb5 against 8480552ae012
(the words are the same)
Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).
Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/Statement.lean. Origin: skeleton-hole.
Depends on (1), each in words
Depends on, each in words where someone has written them:
- erdos-1094--h2--h1--h1--h1: $\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$
Attestation: none of a proof
No proof of this statement has been merged. A partial assembly merged under attestations/000516.json: it records an attempt, not a proof (see Attempts below).
Witness
Not checked — no run on this page records step 7 passing for it.
1aa8a1c1b9f3.import Mathlib open scoped Nat theorem witness : True := trivial
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 →
Attempts (1)
1 recorded. Routes refuted: none. Failure classes: none.
Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.
Untrusted: partial assembly (D-12 #5), by t1014-y; merged in b76ef98d4e17 under attestations/000516.json, whose step 2 took this file as a partial. A partial records an attempt, not a proof: the gate replayed it with its holes left as sorry. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/attempts/20261014T111741Z-t1014-y-partial.lean.
Untrusted contributor text — an outline the gate extracted from this partial assembly; its holes are sorry steps, and it records an attempt, not a proof.
Outline of 20261014T111741Z-t1014-y-partial.lean, extracted by the gate at f97b6921b55b 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.
h_gcd_minFachave∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (n / n.gcd k).minFac > kLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ K, withh_gcd_minFac : ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (n / n.gcd k).minFac > k.Lean, lines 13–42
have h_gcd_minFac : ∀ (n k : ℕ), 0 < k → 2 * k ≤ n → (n.choose k).minFac > k → (n / n.gcd k).minFac > k := by intro n k hk hn hm have hn0 : 0 < n := by omega have hkn : k ≤ n := by omega set g := n.gcd k with hg have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0 have hgn : g ∣ n := Nat.gcd_dvd_left n k have hgk : g ∣ k := Nat.gcd_dvd_right n k have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by have := Nat.add_one_mul_choose_eq (n - 1) (k - 1) rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0 have hdvd : n / g ∣ n.choose k := by have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm exact hcop.dvd_of_dvd_mul_right h1 have h2k : 2 ≤ n / k := (Nat.le_div_iff_mul_le hk).2 (by omega) have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0 have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le have hqC : (n.choose k).minFac ≤ (n / g).minFac := Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd) omegah_gcd_minFac.hn0have(0 : ℕ) < nroutine: omegaLeaves
(n / n.gcd k).minFac > k, withhn0 : (0 : ℕ) < n.Lean, line 16
have hn0 : 0 < n := by omega
h_gcd_minFac.hknhavek ≤ nroutine: omegaLeaves
(n / n.gcd k).minFac > k, withhkn : k ≤ n.Lean, line 17
have hkn : k ≤ n := by omega
h_gcd_minFac.hg0have(0 : ℕ) < gLeaves
(n / g).minFac > k, withhg0 : (0 : ℕ) < g.Uses library
Nat.gcd_pos_of_pos_left.Lean, line 19
have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
h_gcd_minFac.hgnhaveg ∣ nLeaves
(n / g).minFac > k, withhgn : g ∣ n.Uses library
Nat.gcd_dvd_left.Lean, line 20
have hgn : g ∣ n := Nat.gcd_dvd_left n k
h_gcd_minFac.hgkhaveg ∣ kLeaves
(n / g).minFac > k, withhgk : g ∣ k.Uses library
Nat.gcd_dvd_right.Lean, line 21
have hgk : g ∣ k := Nat.gcd_dvd_right n k
h_gcd_minFac.hidhaven * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * kLeaves
(n / g).minFac > k, withhid : n * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * k.Uses library
Nat.sub_add_cancel.Lean, lines 22–24
have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by have := Nat.add_one_mul_choose_eq (n - 1) (k - 1) rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at thish_gcd_minFac.hid.thishave(n - (1 : ℕ) + (1 : ℕ)) * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = (n - (1 : ℕ) + (1 : ℕ)).choose (k - (1 : ℕ) + (1 : ℕ)) * (k - (1 : ℕ) + (1 : ℕ))Leaves
n * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * k, withthis : (n - (1 : ℕ) + (1 : ℕ)) * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = (n - (1 : ℕ) + (1 : ℕ)).choose (k - (1 : ℕ) + (1 : ℕ)) * (k - (1 : ℕ) + (1 : ℕ)).Uses library
Nat.add_one_mul_choose_eq.Lean, line 23
have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
h_gcd_minFac.hcophave(n / g).Coprime (k / g)Leaves
(n / g).minFac > k, withhcop : (n / g).Coprime (k / g).Uses library
Nat.Coprimemandnare coprime, or relatively prime, if theirgcdis 1. ,Nat.coprime_div_gcd_div_gcd.Lean, line 25
have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
h_gcd_minFac.hdvdhaven / g ∣ n.choose kLeaves
(n / g).minFac > k, withhdvd : n / g ∣ n.choose k.Lean, lines 26–36
have hdvd : n / g ∣ n.choose k := by have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm exact hcop.dvd_of_dvd_mul_right h1h_gcd_minFac.hdvd.h1haven / g ∣ n.choose k * (k / g)Leaves
n / g ∣ n.choose k, withh1 : n / g ∣ n.choose k * (k / g).Uses library
Exists.introExistential introduction. ,Nat.eq_of_mul_eq_mul_right.Lean, lines 27–35
have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symmh_gcd_minFac.hdvd.h1.e1haven = n / g * gLeaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withe1 : n = n / g * g.Uses library
Nat.div_mul_cancel.Lean, line 29
have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
h_gcd_minFac.hdvd.h1.e2havek = k / g * gLeaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withe2 : k = k / g * g.Uses library
Nat.div_mul_cancel.Lean, line 30
have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
h_gcd_minFac.hdvd.h1.s3haven / g * g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * (k / g * g)Leaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withthis : n / g * g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * (k / g * g).Lean, lines 31–32
have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hidh_gcd_minFac.hdvd.h1.s4haven / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) * g = n.choose k * (k / g) * gLeaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withthis : n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) * g = n.choose k * (k / g) * g.Lean, lines 33–34
have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this
h_gcd_minFac.h2khave(2 : ℕ) ≤ n / kLeaves
(n / g).minFac > k, withh2k : (2 : ℕ) ≤ n / k.Uses library
Nat.le_div_iff_mul_le.Lean, line 37
have h2k : 2 ≤ n / k := (Nat.le_div_iff_mul_le hk).2 (by omega)
h_gcd_minFac.hnghaven / k ≤ n / gLeaves
(n / g).minFac > k, withhng : n / k ≤ n / g.Uses library
Nat.div_le_div_left,Nat.le_of_dvd.Lean, line 38
have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
h_gcd_minFac.hq2have(2 : ℕ) ≤ (n / g).minFacLeaves
(n / g).minFac > k, withhq2 : (2 : ℕ) ≤ (n / g).minFac.Uses library
Nat.minFac_prime.Lean, line 39
have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
h_gcd_minFac.hqChave(n.choose k).minFac ≤ (n / g).minFacLeaves
(n / g).minFac > k, withhqC : (n.choose k).minFac ≤ (n / g).minFac.Uses library
Nat.minFac_le_of_dvd,Nat.minFac_dvd.Lean, lines 40–41
have hqC : (n.choose k).minFac ≤ (n / g).minFac := Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
h_gphole∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ KholeLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ K, withh_gp : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K.Left open as a hole; its statement is erdos-1094--h2--h1--h1--h1 (open).
Lean, lines 45–47
have h_gp : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by sorrys3obtain∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ KLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ K, withK : ℕ,hK : ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K.Lean, line 48
obtain ⟨K, hK⟩ := h_gp
closeterm∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ KCloses the goal.
Uses library
Exists.introExistential introduction. .Lean, line 49
exact ⟨K, fun n k hk hn hc hm => hK n k hk hn hc hm (h_gcd_minFac n k hk hn hm)⟩
import Mathlib
import Nodes.«erdos-1094--h2--h1--h1».Context
open scoped Nat
/-! Hole `h_good_below_cube` of a merged partial proof, as a node (D-12 #5, D-29).
Statement generated by the gate from the assembly; immutable (D-3). -/
theorem erdos_1094__h2__h1__h1 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → k ≤ K := by
-- Proved here (assembly): n / gcd(n,k) divides C(n,k) (from k*C(n,k) = n*C(n-1,k-1) and
-- coprimality of n/g and k/g), and n/g ≥ n/k ≥ 2, so its least prime factor is at least
-- minFac C(n,k) > k: every prime factor of n / gcd(n,k) exceeds k.
have h_gcd_minFac : ∀ (n k : ℕ), 0 < k → 2 * k ≤ n → (n.choose k).minFac > k →
(n / n.gcd k).minFac > k := by
intro n k hk hn hm
have hn0 : 0 < n := by omega
have hkn : k ≤ n := by omega
set g := n.gcd k with hg
have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
have hgn : g ∣ n := Nat.gcd_dvd_left n k
have hgk : g ∣ k := Nat.gcd_dvd_right n k
have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by
have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
have hdvd : n / g ∣ n.choose k := by
have h1 : n / g ∣ n.choose k * (k / g) := by
refine ⟨(n - 1).choose (k - 1), ?_⟩
have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by
rw [← e1, ← e2]; exact hid
have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by
linear_combination this
exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
exact hcop.dvd_of_dvd_mul_right h1
have h2k : 2 ≤ n / k := (Nat.le_div_iff_mul_le hk).2 (by omega)
have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
have hqC : (n.choose k).minFac ≤ (n / g).minFac :=
Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
omega
-- The open half: the same statement, given in addition that every prime factor of
-- n / gcd(n,k) exceeds k.
have h_gp : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k →
(n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
sorry
obtain ⟨K, hK⟩ := h_gp
exact ⟨K, fun n k hk hn hc hm => hK n k hk hn hc hm (h_gcd_minFac n k hk hn hm)⟩Annexes (2), in full
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by t1014-y, drafted with claude-opus-5-5 via Claude Code, 2026-10-14T11:24:33Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/annex/30caffb978c4606840b5f7ef64364716b471a737895400552240b538156b48e0.md.
Structure forced by the hypotheses (B, t1014-y, 2026-10-14). The divisibility claim below is proved in Lean in the assemblies of PRs #514, #515, #516; the remarks after it are mine and NOT machine-checked.
Fact (proved in Lean). Let g = gcd(n,k). From k*C(n,k) = n*C(n-1,k-1) and gcd(n/g, k/g) = 1, n/g divides C(n,k). Hence minFac C(n,k) <= minFac(n/g) whenever n/g >= 2.
Consequences.
- On --h2--h1--h1 (2k <= n < k^3, minFac C(n,k) > k): every prime factor of n/gcd(n,k) exceeds k (PR #516's hole carries this as a hypothesis). Unchecked remark: if moreover k | n, then n/k < k^2 has all prime factors > k, so n/k is a prime in (k, k^2); in general n = g*m with g | k and m a product of at most two primes above k (since m < k^3/g).
- On --h2--h1--h4 and --h2--h2--h3 (k^2 <= n, minFac C(n,k) > n/k): n/gcd(n,k) is prime (PR #514, #515). So n = g*p with g | k, g < k and p a prime > n/k. Unchecked remark: then floor(n/k) = floor(g*p/k), and the hypothesis k*floor(n/k) | k! says floor(n/k) has all prime factors < k.
Suggested next step for a successor (unchecked): on the holes, split on g = gcd(n,k). For g = 1 (n coprime to k) the hole is about primes-free windows; for g > 1 write n = g*p and apply Kummer's theorem prime by prime for p' <= k (no carries when adding k and n-k in base p').
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission, 2026-10-14T07:33:43Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h1/annex/af52fe7a6ac3a75df376852c36d02642c2969d89350d2b7cc853b0373c752d67.md.
Numerical check (2026-10-12, finite range, not a proof): smallest working $K$ in range $35$; pairs found: 137 pairs.
- Range searched: every $k\le 1000$, every $n$ with $2k\le n<k^3$ (complete in that range).
- Pairs $(n,k)$ found that force $K\ge k$: 137 pairs, the largest $(6459,33)$ and $(37619,35)$; none for $36\le k\le 1000$.
- Smallest $K$ that works in this range: $35$.
The method, the cross-checks and the code are in the numerical annex on erdos-1094 (the root), dated 2026-10-12.
How to read this page
No explainer yet. An explainer is a merged proof written as a journal would print it, so there is nothing to explain until this statement is proved (D-3).