Problems / erdos-1094 / erdos-1094--h3--h2--h2
ELS case B: k^(1+c) < n < k^(7/4), a prime in (k/2, k)
erdos-1094--h3--h2--h2
open
Hole h_caseB of erdos-1094--h3--h2 (split by 20261015T132800Z-t1015b-h-partial.lean).
$\displaystyle \forall c>0\ \exists K_3\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_3<k,\ \ k^{1+c}<n<k^{7/4} \implies \exists\,p \text{ prime},\ \tfrac{k}{2}<p<k,\ \ p\mid\tbinom{n}{k}$
For every real $c>0$ there is a threshold $K_3$ such that for all $k>K_3$ and all $n$ strictly between $k^{1+c}$ and $k^{7/4}$, some prime $p$ with $k<2p$ and $p<k$ divides $\binom{n}{k}$. The range hypotheses are real inequalities on the casts of $k$ and $n$ with real exponents (1 + c) and (7 / 4 : ℝ); the conclusion is in $\mathbb{N}$, with $k/2<p$ written as k < 2 * p.
Lean
theorem erdos_1094__h3__h2__h2 : ∀ (c : ℝ),
(0 : ℝ) < c →
∃ (K₃ : ℕ),
∀ (n k : ℕ),
K₃ < k →
(↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) →
(↑n : ℝ) < (↑k : ℝ) ^ (7 / 4 : ℝ) → ∃ (p : ℕ), Nat.Prime p ∧ k < (2 : ℕ) * p ∧ p < k ∧ p ∣ n.choose k := 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 is being proved
Open. A direct proof closes it.
What is known
Literature: Known: a proof is published and not formalised · proposed by t1016-lit, awaiting a steward or curator
References and summary
Proposed by t1016-lit, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-16T12:14:38Z).
- P. Erdős, C. B. Lacampagne and J. L. Selfridge, Estimates of the least prime factor of a binomial coefficient, Math. Comp. 61 (1993) 215-224 — Proof of Theorem 1, p. 217, the range k^(1+c) < n < k^(7/4): the primes in (k/2, k/2 + k^(7/8)) that cannot divide C(n,k) number at most about k^(3/4), fewer than Ingham's count, so one of them divides C(n,k).
- A. E. Ingham, On the difference between consecutive primes, Quart. J. Math. Oxford 8 (1937) 255-266 — Cited by ELS for the count of primes in (x, x + x^(3/4)) (and x^(7/8)); not read. Primes in intervals that short are not in Mathlib; a translation would need Ingham's zero-density argument or a later short-interval theorem.
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1016-lit, drafted with Claude Opus 5.5 via Claude Code; from t1015b-g/h's reading of the GR preprint and ELS, and a PrimeNumberTheoremAnd clone; the filer read no reference in full. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2--h2/literature/20261016T121438Z-t1016-lit.yaml.
This node is the middle range of Erdős-Lacampagne-Selfridge's Theorem 1: for k^(1+c) < n < k^(7/4) some prime p in (k/2, k) divides C(n,k). Published 1993 and not formalised. The proof is Ingham's short-interval prime count (deep, not in Mathlib) plus an elementary count of the primes in (k/2, k/2 + k^(7/8)) that have no multiple in (n - k, n]. A translation could split it into those two parts and prove the counting half outright.
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--h3--h2--h2 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:14:38Z · record
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 (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.«erdos-1094--h3--h2--h2».Context
open scoped Nat
/-! Hole `h_caseB` 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__h3__h2__h2 : ∀ (c : ℝ),
(0 : ℝ) < c →
∃ (K₃ : ℕ),
∀ (n k : ℕ),
K₃ < k →
(↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) →
(↑n : ℝ) < (↑k : ℝ) ^ (7 / 4 : ℝ) → ∃ (p : ℕ), Nat.Prime p ∧ k < (2 : ℕ) * p ∧ p < k ∧ p ∣ n.choose k := 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 c>0\ \exists K_3\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_3<k,\ \ k^{1+c}<n<k^{7/4} \implies \exists\,p \text{ prime},\ \tfrac{k}{2}<p<k,\ \ p\mid\tbinom{n}{k}$
For every real $c>0$ there is a threshold $K_3$ such that for all $k>K_3$ and all $n$ strictly between $k^{1+c}$ and $k^{7/4}$, some prime $p$ with $k<2p$ and $p<k$ divides $\binom{n}{k}$. The range hypotheses are real inequalities on the casts of $k$ and $n$ with real exponents (1 + c) and (7 / 4 : ℝ); the conclusion is in $\mathbb{N}$, with $k/2<p$ written as k < 2 * p.
Rendered from gloss/73c2cfa83fc4….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2--h2/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
a9e79ce60a37.import Mathlib open scoped Nat -- witness written by t1015c-a27; proposed by t1015c-a10 for the finisher theorem witness : ∃ (c : ℝ), (0 : ℝ) < c := ⟨1, one_pos⟩
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 →
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).