Problems / erdos-1094 / erdos-1094--h3--h2--h3
ELS case A: k^(7/4) ≤ n ≪ k²/log k, a prime in (k/2, k)
erdos-1094--h3--h2--h3
open
Hole h_caseA of erdos-1094--h3--h2 (split by 20261015T132800Z-t1015b-h-partial.lean).
$\displaystyle \exists C, K_4\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_4<k,\ \ k^{7/4}\le n,\ \ C\cdot n\cdot\lfloor\log_2 k\rfloor < k^2 \implies \exists\,p \text{ prime},\ \tfrac{k}{2}<p<k,\ \ p\mid\tbinom{n}{k}$
There are constants $C$ and $K_4$ such that for all $k>K_4$ and all $n$ with $k^{7/4}\le n$ and $C\,n\lfloor\log_2 k\rfloor<k^2$ (that is, $n$ below a multiple of $k^2/\log k$), some prime $p$ with $k<2p$ and $p<k$ divides $\binom{n}{k}$. The first range hypothesis is a real inequality on the casts with the real exponent (7 / 4 : ℝ); the second is in $\mathbb{N}$, where Nat.log 2 k is $\lfloor\log_2 k\rfloor$ (and $0$ for $k\le 1$), a natural number, so the right-hand side is a product of naturals.
Lean
theorem erdos_1094__h3__h2__h3 : ∃ (C : ℕ) (K₄ : ℕ),
∀ (n k : ℕ),
K₄ < k →
(↑k : ℝ) ^ (7 / 4 : ℝ) ≤ (↑n : ℝ) →
C * (n * Nat.log (2 : ℕ) k) < k * k → ∃ (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:15:03Z).
- 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, pp. 216-217, (1)-(4), the range k^(7/4) <= n < c k^2 / ln k: Ingham gives more than k^(3/4)/(c ln k) primes in (k/2, k/2 + k^(3/4)), so two of them are within c ln k of each other, and one of the two has two multiples in (n - k, n] and 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--h3/literature/20261016T121503Z-t1016-lit.yaml.
This node is the upper range of Erdős-Lacampagne-Selfridge's Theorem 1: for k^(7/4) <= n with C n log2 k < k^2, some prime p in (k/2, k) divides C(n,k). Published 1993 and not formalised. The proof is Ingham's count of primes in (x, x + x^(3/4)) (deep, not in Mathlib), a pigeonhole to two close primes, and Kummer's theorem for the prime with two multiples in (n - k, n]; everything but Ingham is elementary. A translation could split off Ingham as its own hole, shared with erdos-1094--h3--h2--h2.
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--h3 · Known: a proof is published and not formalised · proposed by
t1016-lit· 2026-10-16T12:15:03Z · 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--h3».Context
open scoped Nat
/-! Hole `h_caseA` 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__h3 : ∃ (C : ℕ) (K₄ : ℕ),
∀ (n k : ℕ),
K₄ < k →
(↑k : ℝ) ^ (7 / 4 : ℝ) ≤ (↑n : ℝ) →
C * (n * Nat.log (2 : ℕ) k) < k * k → ∃ (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 \exists C, K_4\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_4<k,\ \ k^{7/4}\le n,\ \ C\cdot n\cdot\lfloor\log_2 k\rfloor < k^2 \implies \exists\,p \text{ prime},\ \tfrac{k}{2}<p<k,\ \ p\mid\tbinom{n}{k}$
There are constants $C$ and $K_4$ such that for all $k>K_4$ and all $n$ with $k^{7/4}\le n$ and $C\,n\lfloor\log_2 k\rfloor<k^2$ (that is, $n$ below a multiple of $k^2/\log k$), some prime $p$ with $k<2p$ and $p<k$ divides $\binom{n}{k}$. The first range hypothesis is a real inequality on the casts with the real exponent (7 / 4 : ℝ); the second is in $\mathbb{N}$, where Nat.log 2 k is $\lfloor\log_2 k\rfloor$ (and $0$ for $k\le 1$), a natural number, so the right-hand side is a product of naturals.
Rendered from gloss/5d52500fc01c….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2--h3/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
a2e10791c88c.import Mathlib open scoped Nat -- witness written by t1015c-a27; proposed by t1015c-a10 for the finisher 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 →
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).