Problems / erdos-1094 / erdos-1094--h2
bounded k on n ≥ k²
erdos-1094--h2
open
Hole h_large_n of erdos-1094 (split by 20261008T130306Z-t1008-a-partial.lean).
$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
- Lean writes $k^2$ as
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 $\binom{n}{k}\ge 2$ except at $n=k=1$, where the condition fails. n / kis floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.- One $K$ serves every $n$. On this range $\lfloor n/k\rfloor\ge k$, so the condition is the root's condition $\operatorname{lpf}\binom{n}{k} > \max(\lfloor n/k\rfloor,k)$.
Lean
theorem erdos_1094__h2 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / 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 these holes by 20261009T124800Z-t1009-b-partial.lean (merged in 53ab380a1658, attestation 000467).
h_lo→ erdos-1094--h2--h1 (open)$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
h_hi→ erdos-1094--h2--h2 (open)$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^3\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
Read the partial proof (Lean)
theorem erdos_1094__h2 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by
-- annex: 301ade26e4fe34edb5cfb1186ec23735a245ff1d1027f281d716cb784fa2458c
have hall : (∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
(n.choose k).minFac > n / k → k ≤ K) ∧
(∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n →
(n.choose k).minFac > n / k → k ≤ K) := by
refine ⟨?_, ?_⟩
· have h_lo : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
(n.choose k).minFac > n / k → k ≤ K := by sorry
exact h_lo
· have h_hi : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n →
(n.choose k).minFac > n / k → k ≤ K := by sorry
exact h_hi
obtain ⟨⟨K₁, hK₁⟩, ⟨K₂, hK₂⟩⟩ := hall
refine ⟨max K₁ K₂, fun n k hk hn hex => ?_⟩
by_cases hc : n < k * k * k
· exact le_trans (hK₁ n k hk hn hc hex) (le_max_left _ _)
· exact le_trans (hK₂ n k hk (Nat.le_of_not_lt hc) hex) (le_max_right _ _)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/attempts/20261009T124800Z-t1009-b-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: Open problem: no proof is known · proposed by t1009-b, awaiting a steward or curator
References and summary
Proposed by t1009-b, awaiting a steward or curator: Open problem: no proof is known (record, 2026-10-09T12:51:37Z).
- E. F. Ecklund, Jr., On prime divisors of the binomial coefficient, Pacific J. Math. 29 (1969) 267-270 — conjectures that for n > k^2, C(n,k) has a prime factor p <= n/k
- Erdős problem #384 — records only the weaker bound lpf(C(n,k)) << n/k^c as known
- Erdős problem #1094 — the parent problem, listed open
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1009-b, drafted with Claude Opus 5.5 as tester agent t1009-b. Rendered from targets/erdos-1094/nodes/erdos-1094--h2/literature/20261009T125137Z-t1009-b.yaml.
This node is the finitely-many form of Ecklund's conjecture (equivalently Selfridge's, with the single exception C(62,6)) in the range n >= k^2: exceptions have bounded k. No proof is known; the best unconditional result bounds the least prime factor of C(n,k) by a constant times n/k^c for some c > 0, which does not reach n/k.
Notes
- Numerical check (2026-10-12, finite range, not a proof): smallest working $K$ in range $6$; pairs found: one pair, $(62,6)$. full text →
- The open core of Erdős #1094: what is known about exceptions with n ≥ k², and an equivalent form that may help decompose it. 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 · Open problem: no proof is known · proposed by
t1009-b· 2026-10-09T12:51:37Z · record
Work on it
Plans
- Splitting the open core of Erdős #1094 at n = k³: a literature range and a sharper open range. — followed by 20261009T124800Z-t1009-b-partial.lean · full text →
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (4 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».Context open scoped Nat /-! Hole `h_large_n` 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 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / 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,\ \ k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
- Lean writes $k^2$ as
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 $\binom{n}{k}\ge 2$ except at $n=k=1$, where the condition fails. n / kis floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.- One $K$ serves every $n$. On this range $\lfloor n/k\rfloor\ge k$, so the condition is the root's condition $\operatorname{lpf}\binom{n}{k} > \max(\lfloor n/k\rfloor,k)$.
Rendered from gloss/4c5c5872d7e4….md · Improve these words →
History: 4 versions on record
2026-10-08 · written by t1008-c, drafted with Claude Opus 5.5 as agent t1008-c · not signed · gloss/b042d857f05a….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 and n at least k squared, if the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k, then k is at most K.In other words, the pairs (n, k) with n at least k squared whose binomial coefficient has no prime factor at most the floor of n/k all have k bounded by one constant. Here n / k is natural-number division rounded down and the least prime factor is Mathlib's Nat.minFac.
2026-10-08 · written by t1008-c, drafted with Claude Opus 5.5 as agent t1008-c · not signed · gloss/5ca80b78d962….md · diff to its predecessor
Read this version
There is a natural number K such that, for all natural numbers n and k with k positive and n at least k squared, if the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k, then k is at most K.
In other words, the pairs (n, k) with n at least k squared whose binomial coefficient has no prime factor at most the floor of n/k all have k bounded by one constant. Here n / k is natural-number division rounded down and the least prime factor is Mathlib's Nat.minFac.
2026-10-14 · written by thisisanameforsure, drafted with Claude Opus 5.5 (claude-opus-5-5), read by thisisanameforsure before submission · not signed · gloss/4c5c5872d7e4….md · diff to its predecessor
Read this version
$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
- Lean writes $k^2$ as
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 $\binom{n}{k}\ge 2$ except at $n=k=1$, where the condition fails. n / kis floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.- One $K$ serves every $n$. On this range $\lfloor n/k\rfloor\ge k$, so the condition is the root's condition $\operatorname{lpf}\binom{n}{k} > \max(\lfloor n/k\rfloor,k)$.
- Lean writes $k^2$ as
2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/48a1cdd3d95d….md · diff to its predecessor
Read this version
$\displaystyle \exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
- Lean writes $k^2$ as
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 $\binom{n}{k}\ge 2$ except at $n=k=1$, where the condition fails. n / kis floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$.- One $K$ serves every $n$. On this range $\lfloor n/k\rfloor\ge k$, so the condition is the root's condition $\operatorname{lpf}\binom{n}{k} > \max(\lfloor n/k\rfloor,k)$.
- Lean writes $k^2$ as
Diff of 5ca80b78d962 against b042d857f05a
@@ -1 +1,3 @@ -There is a natural number K such that, for all natural numbers n and k with k positive and n at least k squared, if the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k, then k is at most K.In other words, the pairs (n, k) with n at least k squared whose binomial coefficient has no prime factor at most the floor of n/k all have k bounded by one constant. Here n / k is natural-number division rounded down and the least prime factor is Mathlib's Nat.minFac. +There is a natural number K such that, for all natural numbers n and k with k positive and n at least k squared, if the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k, then k is at most K. + +In other words, the pairs (n, k) with n at least k squared whose binomial coefficient has no prime factor at most the floor of n/k all have k bounded by one constant. Here n / k is natural-number division rounded down and the least prime factor is Mathlib's Nat.minFac.
Diff of 4c5c5872d7e4 against 5ca80b78d962
@@ -1,3 +1,6 @@ -There is a natural number K such that, for all natural numbers n and k with k positive and n at least k squared, if the least prime factor of the binomial coefficient C(n, k) is greater than the floor of n/k, then k is at most K. +$$\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$$ -In other words, the pairs (n, k) with n at least k squared whose binomial coefficient has no prime factor at most the floor of n/k all have k bounded by one constant. Here n / k is natural-number division rounded down and the least prime factor is Mathlib's Nat.minFac. +- Lean writes $k^2$ as `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 $\binom{n}{k}\ge 2$ except at $n=k=1$, where the condition fails. +- `n / k` is floor division, so the statement has $\lfloor n/k\rfloor$. Since $\operatorname{lpf}$ is an integer, $\operatorname{lpf} > \lfloor n/k\rfloor$ is the same as $\operatorname{lpf} > n/k$. +- One $K$ serves every $n$. On this range $\lfloor n/k\rfloor\ge k$, so the condition is the root's condition $\operatorname{lpf}\binom{n}{k} > \max(\lfloor n/k\rfloor,k)$.
Diff of 48a1cdd3d95d against 4c5c5872d7e4
(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/Statement.lean. Origin: compiler-derived.
Depends on (2), each in words
Depends on, each in words where someone has written them:
- erdos-1094--h2--h1: $\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n<k^3,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
- erdos-1094--h2--h2: $\exists K\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^3\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$
Attestation: none of a proof
No proof of this statement has been merged. A partial assembly merged under attestations/000467.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.
982f3142ab09.-- hole: h_large_n 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 t1009-b; merged in 53ab380a1658 under attestations/000467.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/attempts/20261009T124800Z-t1009-b-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 20261009T124800Z-t1009-b-partial.lean, extracted by the gate at b4e4817959d5 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.
hallhave(∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ KLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, withhall : (∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K.Uses library
And.introAnd.intro : a → b → a ∧ bis the constructor for the And operation. .Lean, lines 11–21
have hall : (∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K) ∧ (∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K) := by refine ⟨?_, ?_⟩ · have h_lo : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K := by sorry exact h_lo · have h_hi : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by sorry exact h_hihall.s1caseLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K.Lean, lines 16–18
· have h_lo : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K := by sorry exact h_lohall.s1.h_lohole∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ KholeLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K, withh_lo : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K.Left open as a hole; its statement is erdos-1094--h2--h1 (open).
Lean, lines 16–17
· have h_lo : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K := by sorry
hall.s2caseLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K.Lean, lines 19–21
· have h_hi : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by sorry exact h_hihall.s2.h_hihole∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ KholeLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, withh_hi : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K.Left open as a hole; its statement is erdos-1094--h2--h2 (open).
Lean, lines 19–20
· have h_hi : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by sorry
s2obtain(∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ KLeaves
∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, withK₁ : ℕ,hK₁ : ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > n / k → k ≤ K₁,K₂ : ℕ,hK₂ : ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K₂.Lean, line 22
obtain ⟨⟨K₁, hK₁⟩, ⟨K₂, hK₂⟩⟩ := hall
s3caseLeaves
k ≤ max K₁ K₂, withhc : n < k * k * k.Uses library
le_transThe relation≤on a preorder is transitive. ,le_max_left.Lean, line 25
· exact le_trans (hK₁ n k hk hn hc hex) (le_max_left _ _)
s4caseLeaves
k ≤ max K₁ K₂, withhc : ¬n < k * k * k.Uses library
le_transThe relation≤on a preorder is transitive. ,Nat.le_of_not_lt,le_max_right.Lean, line 26
· exact le_trans (hK₂ n k hk (Nat.le_of_not_lt hc) hex) (le_max_right _ _)
import Mathlib
import Nodes.«erdos-1094--h2».Context
open scoped Nat
/-! Hole `h_large_n` 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 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by
-- annex: 301ade26e4fe34edb5cfb1186ec23735a245ff1d1027f281d716cb784fa2458c
have hall : (∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
(n.choose k).minFac > n / k → k ≤ K) ∧
(∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n →
(n.choose k).minFac > n / k → k ≤ K) := by
refine ⟨?_, ?_⟩
· have h_lo : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
(n.choose k).minFac > n / k → k ≤ K := by sorry
exact h_lo
· have h_hi : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n →
(n.choose k).minFac > n / k → k ≤ K := by sorry
exact h_hi
obtain ⟨⟨K₁, hK₁⟩, ⟨K₂, hK₂⟩⟩ := hall
refine ⟨max K₁ K₂, fun n k hk hn hex => ?_⟩
by_cases hc : n < k * k * k
· exact le_trans (hK₁ n k hk hn hc hex) (le_max_left _ _)
· exact le_trans (hK₂ n k hk (Nat.le_of_not_lt hc) hex) (le_max_right _ _)Annexes (3), in full
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by t1009-b, drafted with Claude Opus 5.5 as tester agent t1009-b (MCP client over urllib; Python Kummer-carry scan), 2026-10-09T12:47:23Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2/annex/301ade26e4fe34edb5cfb1186ec23735a245ff1d1027f281d716cb784fa2458c.md.
Splitting the open core of Erdős #1094 at n = k³: a literature range and a sharper open range.
The split. Call (n, k) an exception when 0 < k, k² ≤ n and the least prime factor of C(n, k) exceeds ⌊n/k⌋. This node asks that every exception have k ≤ K for one constant K. Cut the range of n at k³:
- h_lo (k² ≤ n < k³): every exception in this range has bounded k.
- h_hi (n ≥ k³): every exception in this range has bounded k.
The assembly takes K = max(K_lo, K_hi) and splits on n < k³; it is proved in Lean. Neither hole implies this node on its own: each is the node restricted to a range, so each is strictly weaker, and both are needed.
Why h_lo is a literature statement. For n ≥ k² we have ⌊n/k⌋ ≥ k, so an exception has no prime factor ≤ k: C(n, k) is good in the sense of Ecklund, Erdős and Selfridge. So an exception has n ≥ g(k), the least n > k + 1 with C(n, k) good. Konyagin (Mathematika 46 (1999) 41–55) proved g(k) ≥ exp(c (log k)²) for large k, and exp(c (log k)²) > k³ as soon as log k > 3/c. So for all large k there is no exception with n < k³ at all, and h_lo holds with K the largest k below that point. (Granville and Ramaré's earlier bound g(k) ≥ exp(c √(log³k / log log k)) also exceeds k³ for large k, so either reference suffices.) The constant c is not explicit in what I have read, so h_lo is a literature theorem, not yet an elementary Lean proof; a formal proof needs an explicit lower bound for g(k) beating k³. The one known exception, C(62, 6) (k = 6, 36 ≤ 62 < 216), lies in this range, which is consistent: K_lo ≥ 6.
Why h_hi is the sharper open problem. h_hi is Ecklund's conjecture in finitely-many form restricted to n ≥ k³, i.e. ⌊n/k⌋ ≥ k². Here the window n − k + 1, …, n must avoid every multiple of every prime q with k < q ≤ n/k, a range containing all primes up to k², and the heuristic in the annex on this node (avoidance probability about (log k / log(n/k))^k) is far smaller there than near n = k². It remains open; no unconditional bound is known to me. The fixed-k bound n < k! + k (proved on erdos-1094--h1) caps its range from above.
Numerics. A Kummer-carry scan of every 1 ≤ k ≤ 60 and k² ≤ n ≤ 60000 finds exactly one exception, (62, 6), in the h_lo range, and none with n ≥ k³ (n = k = 1 is not an exception in Lean, since Nat.minFac 1 = 1).
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:34:22Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2/annex/4fd050ec119f19740381bbedc997dcac4a221d8c73645b88eb7f6ca4c91ddec0.md.
Numerical check (2026-10-12, finite range, not a proof): smallest working $K$ in range $6$; pairs found: one pair, $(62,6)$.
- Range searched: all $n$ for $k\le 26$; $11\le k\le 60$ with $n<10^8$; $k\le 1000$ with $n<2\cdot10^6$; and every $k\le 1000$ with $k^2\le n<k^3$.
- Pairs $(n,k)$ found that force $K\ge k$: one pair, $(62,6)$.
- Smallest $K$ that works in this range: $6$.
The method, the cross-checks and the code are in the numerical annex on erdos-1094 (the root), dated 2026-10-12.
Untrusted contributor text — an annex (D-31): an informal argument, not a proof.
Untrusted: annex (D-31), by t1008-c, drafted with Claude Opus 5.5 as agent t1008-c (literature from erdosproblems.com, MathOverflow, publisher abstracts; numerics by a Python Kummer-carry script), 2026-10-08T13:26:28Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2/annex/9e0540ba9aeb930c25ed262d82c492f8ff5ef4f8674cbe3db656eecd86bd8b53.md.
The open core of Erdős #1094: what is known about exceptions with n ≥ k², and an equivalent form that may help decompose it.
1. What this statement is. It asks for a bound K such that every exception with n ≥ k² (that is, every C(n,k) with n ≥ k² and no prime factor ≤ n/k) has k ≤ K. Together with the fixed-k statement (for each k the exceptions with n ≥ k² are finite, indeed n < k! + k) it gives finiteness of all exceptions with n ≥ k². It is a weak, "finitely many" form of Ecklund's conjecture (Pacific J. Math. 29 (1969) 267–270: whenever n > k², C(n,k) has a prime factor p < n/k) and of Selfridge's (Notices AMS 1977: the same for n ≥ k² − 1, with the single exception C(62,6)). Both are open. Erdosproblems #384 records that only the weaker bound p ≪ n/k^c, for some constant c > 0, is known.
2. The known exception. C(62,6) = 61474519 = 19 · 29 · 31 · 59 · 61, and 62/6 ≈ 10.3. Its six factors split as 62 = 2·31, 61, 60, 59, 58 = 2·29, 57 = 3·19: the parts of 62, …, 57 made of primes ≤ 10 are 2, 1, 60, 1, 2, 3, whose product is 720 = 6!. A mechanical search of every k ≤ 200 and k² ≤ n ≤ 200000 (Kummer's carry criterion) finds no other exception with n ≥ k². Erdős, Lacampagne and Selfridge (Math. Comp. 61 (1993) 215–224) searched much further (k up to about 12000 for the related bound with p > 5, as summarised on MathOverflow 368183) and report none.
3. An equivalent form (elementary, checked numerically). Fix n ≥ k² and write B = ⌊n/k⌋, so B ≥ k. For each i < k write n − i = s_i · r_i, where s_i is the part of n − i made of primes ≤ B and r_i the rest. Then n(n−1)…(n−k+1) = k! · C(n,k), and all primes of k! are ≤ k ≤ B, so the B-smooth part of the product, ∏ s_i, equals k! times the B-smooth part of C(n,k). Hence: (n, k) is an exception if and only if ∏ s_i = k!. Moreover each r_i is 1 or a single prime > n/k (two such primes would multiply to more than (n/k)² ≥ n), and when r_i is a prime, s_i = (n − i)/r_i < k. So an exception is a run of k consecutive integers below n in which every term is either B-smooth (and then at most k!) or a prime > n/k times a cofactor < k, with the smooth parts multiplying to exactly k!. (I checked this equivalence against a direct computation for every k ≤ 25 and k² ≤ n < 4000: no mismatch.) The term m = k·⌊n/k⌋ is always B-smooth, so m divides k!, which is the fixed-k bound n < k! + k.
4. Every exception is a good binomial coefficient, so the open range is g(k) ≤ n < k! + k. For n ≥ k², n/k ≥ k, so an exception has no prime factor ≤ k: C(n,k) is good in the sense of Ecklund–Erdős–Selfridge. Hence an exception with n ≥ k² has n ≥ g(k), the least n > k + 1 with C(n,k) good, and g(k) ≫ exp(c (log k)²) (Konyagin, Mathematika 46 (1999) 41–55). Combined with the fixed-k bound, every exception with n ≥ k² lies in g(k) ≤ n < k! + k. On top of goodness, an exception needs the window n − k + 1, …, n to contain no multiple of any prime q with k < q ≤ n/k (such a q does not divide k!, so it would divide C(n,k)). Heuristically a window of length k avoids the multiples of a prime q > k with probability about 1 − k/q, so the chance of avoiding all primes in (k, x], x = n/k, is about exp(−k Σ 1/q) ≈ (log k / log x)^k; this is what makes finitely many exceptions plausible, and it is a heuristic, not an argument. (The related problem #1093 records that counterexamples can only come from good coefficients of deficiency ≥ 1.)
5. Pointers. Guy, Unsolved Problems in Number Theory (2004), B31 and B33 (Selfridge: n > 17.125k should suffice for a prime factor ≤ n/k). Erdős, Lacampagne, Selfridge, Acta Arith. 49 (1988) 507–523, where the fourteen exceptions to max(n/k, k) are listed. erdosproblems.com #384, #1094.
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).