Problems / erdos-1094 / erdos-1094--h3--h2--h1

Ecklund–Erdős–Selfridge: n > k^(1+c) when lpf C(n,k) > k

erdos-1094--h3--h2--h1

open

Hole h_ees of erdos-1094--h3--h2 (split by 20261015T132800Z-t1015b-h-partial.lean).

$\displaystyle \exists c\in\mathbb{R},\ c>0,\ \exists K_2\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n,\ \ \operatorname{minFac}\tbinom{n}{k}>k \implies k^{1+c} < n$

There is an absolute real $c>0$ and a threshold $K_2$ such that for all $k>K_2$ and $n\ge 2k$, if every prime factor of $\binom{n}{k}$ exceeds $k$ then $n$ exceeds $k^{1+c}$. The inequality is in the reals: $k$ and $n$ are cast to $\mathbb{R}$ and $k^{1+c}$ is the real power (↑k : ℝ) ^ (1 + c); $\operatorname{minFac}$ is Mathlib's Nat.minFac, the least prime factor.

unverified · history

Lean

theorem erdos_1094__h3__h2__h1 : ∃ (c : ℝ),
  (0 : ℝ) < c ∧
    ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := 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.

Split into

Proved from this hole by 20261018T193200Z-t1018-c-partial.lean (merged in 92ace71b492d, attestation 000762).

h_lt → erdos-1094--h3--h2--h1--h1 (needs a witness)
$\displaystyle \exists c>0\,\exists K\,\forall n,k:\ K<k,\ 2k\le n<k^2,\ \mathrm{lpf}\binom{n}{k}>k \Rightarrow k^{1+c}<n$

Read the partial proof (Lean)

theorem erdos_1094__h3__h2__h1 : ∃ (c : ℝ),
  (0 : ℝ) < c ∧
    ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := by
  -- approach: n ≥ k² is immediate with c ≤ 1/2; only the range n < k² needs EES
  -- licence: CC-BY-4.0
  -- label: EES bound below k squared
  -- claim: $\exists c>0\,\exists K\,\forall n,k:\ K<k,\ 2k\le n<k^2,\ \mathrm{lpf}\binom{n}{k}>k \Rightarrow k^{1+c}<n$
  -- The Ecklund–Erdős–Selfridge bound restricted to the only range where it has content.
  have h_lt : ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k →
      (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := sorry
  obtain ⟨c, hc, K, hK⟩ := h_lt
  refine ⟨min c (1 / 2), lt_min hc (by norm_num), K + 1, fun n k hk h2 hmf => ?_⟩
  have hk1 : (1 : ℝ) < (k : ℝ) := by exact_mod_cast (show 1 < k by omega)
  by_cases hn : n < k * k
  · calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + c) :=
          Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_left c (1 / 2)])
      _ < (n : ℝ) := hK n k (by omega) h2 hn hmf
  · replace hn := not_lt.mp hn
    have hnk : ((k : ℝ) * k) ≤ (n : ℝ) := by exact_mod_cast hn
    calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + 1 / 2) :=
          Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_right c (1 / 2)])
      _ < (k : ℝ) ^ (2 : ℝ) := Real.rpow_lt_rpow_of_exponent_lt hk1 (by norm_num)
      _ = (k : ℝ) * k := by rw [Real.rpow_two, sq]
      _ ≤ (n : ℝ) := hnk

The gate replayed this file at its merge, each hole a sorry (D-12 #5); the whole file: targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-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 t1016-lit, awaiting a steward or curator

References and summary

Literature status

Proposed by t1016-lit, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-16T12:14:34Z).

E. F. Ecklund, P. Erdős and J. L. Selfridge, A new function associated with the prime factors of (n choose k), Math. Comp. 28 (1974) 647-649 — Proves g(k) > k^(1+c) for an absolute c > 0, where g(k) is the least n > k+1 with every prime factor of C(n,k) above k. Not read; the statement is as ELS 1993 and an earlier annex on erdos-1094--h3 quote it.
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 — Cites EES 1974 for the range n <= k^(1+c) in the proof of its Theorem 1 (p. 216).

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--h1/literature/20261016T121434Z-t1016-lit.yaml.

This node is the Ecklund-Erdős-Selfridge bound: if 2k <= n and C(n,k) has no prime factor <= k, then n > k^(1 + c) for large k. Published 1974 and not formalised. The filer has not read the proof; a translator should read EES 1974 first (three pages) and judge whether it is elementary (Sylvester-Schur style counting of prime powers in k! against the product (n-k+1)...n) before attempting it. Of the three ELS ranges this is the likeliest to be within reach.

Work on it

Work on this statement →

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--h1».Context

open scoped Nat

/-! Hole `h_ees` 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__h1 : ∃ (c : ℝ),
  (0 : ℝ) < c ∧
    ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := by
  sorry

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\in\mathbb{R},\ c>0,\ \exists K_2\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_2<k,\ \ 2k\le n,\ \ \operatorname{minFac}\tbinom{n}{k}>k \implies k^{1+c} < n$

Rendered from gloss/0b5734e7bd93….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/Statement.lean. Origin: compiler-derived.

Depends on (1), each in words

Depends on, each in words where someone has written them:

erdos-1094--h3--h2--h1--h1: $\exists c>0\,\exists K\,\forall n,k:\ K<k,\ 2k\le n<k^2,\ \mathrm{lpf}\binom{n}{k}>k \Rightarrow k^{1+c}<n$

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000762.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.

Witness.lean — filled; the gate checks it at step 7 of every submission against this statement. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/Witness.lean, sha256 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 →

Attempts (2)

2 recorded. Routes refuted: none. Failure classes: missing-library 1.

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 t1018-c; merged in 92ace71b492d under attestations/000762.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--h3--h2--h1/attempts/20261018T193200Z-t1018-c-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 20261018T193200Z-t1018-c-partial.lean, extracted by the gate at 32961c7678e9 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_lt hole ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) hole
Leaves ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ), with h_lt : ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ).
Left open as a hole; its statement is erdos-1094--h3--h2--h1--h1 (needs a witness).
Lean, lines 17–18
```
  have h_lt : ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k →
      (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := sorry
```
targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, lines 17–18 at 6ba7fea98468 ↗
s2 obtain ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ)
Leaves ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ), with c : ℝ, hc : (0 : ℝ) < c, K : ℕ, hK : ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ).
Lean, line 19
```
  obtain ⟨c, hc, K, hK⟩ := h_lt
```
targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, line 19 at 6ba7fea98468 ↗
hk1 have (1 : ℝ) < (↑k : ℝ)
Leaves (↑k : ℝ) ^ ((1 : ℝ) + min c (1 / 2 : ℝ)) < (↑n : ℝ), with hk1 : (1 : ℝ) < (↑k : ℝ).
Lean, line 21
```
  have hk1 : (1 : ℝ) < (k : ℝ) := by exact_mod_cast (show 1 < k by omega)
```
targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, line 21 at 6ba7fea98468 ↗
s4 case
Leaves (↑k : ℝ) ^ ((1 : ℝ) + min c (1 / 2 : ℝ)) < (↑n : ℝ), with hn : n < k * k.
Lean, lines 23–25
```
  · calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + c) :=
          Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_left c (1 / 2)])
      _ < (n : ℝ) := hK n k (by omega) h2 hn hmf
```
targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, lines 23–25 at 6ba7fea98468 ↗
1. s4.s1 calc (↑k : ℝ) ^ ((1 : ℝ) + min c (1 / 2 : ℝ)) ≤ (↑k : ℝ) ^ ((1 : ℝ) + c)
  Closes the goal.
  Uses library Min.min, Real.rpow_le_rpow_of_exponent_le, min_le_left.
  Lean, lines 23–24
  · calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + c) := Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_left c (1 / 2)])
  targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, lines 23–24 at 6ba7fea98468 ↗
2. s4.s2 calc (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ)
  Closes the goal.
  Lean, line 25
  _ < (n : ℝ) := hK n k (by omega) h2 hn hmf
  targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, line 25 at 6ba7fea98468 ↗
s5 case
Leaves (↑k : ℝ) ^ ((1 : ℝ) + min c (1 / 2 : ℝ)) < (↑n : ℝ), with hn : ¬n < k * k.
Uses library not_lt.
Lean, lines 26–32
```
  · replace hn := not_lt.mp hn
    have hnk : ((k : ℝ) * k) ≤ (n : ℝ) := by exact_mod_cast hn
    calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + 1 / 2) :=
          Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_right c (1 / 2)])
      _ < (k : ℝ) ^ (2 : ℝ) := Real.rpow_lt_rpow_of_exponent_lt hk1 (by norm_num)
      _ = (k : ℝ) * k := by rw [Real.rpow_two, sq]
      _ ≤ (n : ℝ) := hnk
```
targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, lines 26–32 at 6ba7fea98468 ↗
1. s5.hnk have (↑k : ℝ) * (↑k : ℝ) ≤ (↑n : ℝ)
  Leaves (↑k : ℝ) ^ ((1 : ℝ) + min c (1 / 2 : ℝ)) < (↑n : ℝ), with hnk : (↑k : ℝ) * (↑k : ℝ) ≤ (↑n : ℝ).
  Lean, line 27
  have hnk : ((k : ℝ) * k) ≤ (n : ℝ) := by exact_mod_cast hn
  targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, line 27 at 6ba7fea98468 ↗
2. s5.s2 calc (↑k : ℝ) ^ ((1 : ℝ) + min c (1 / 2 : ℝ)) ≤ (↑k : ℝ) ^ ((1 : ℝ) + (1 / 2 : ℝ))
  Closes the goal.
  Uses library Min.min, Real.rpow_le_rpow_of_exponent_le, min_le_right.
  Lean, lines 28–29
  calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + 1 / 2) := Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_right c (1 / 2)])
  targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, lines 28–29 at 6ba7fea98468 ↗
3. s5.s3 calc (↑k : ℝ) ^ ((1 : ℝ) + (1 / 2 : ℝ)) < (↑k : ℝ) ^ (2 : ℝ)
  Closes the goal.
  Uses library Real.rpow_lt_rpow_of_exponent_lt.
  Lean, line 30
  _ < (k : ℝ) ^ (2 : ℝ) := Real.rpow_lt_rpow_of_exponent_lt hk1 (by norm_num)
  targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, line 30 at 6ba7fea98468 ↗
4. s5.s4 calc
  Closes the goal.
  Uses library Real.rpow_two, sq.
  Lean, line 31
  _ = (k : ℝ) * k := by rw [Real.rpow_two, sq]
  targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, line 31 at 6ba7fea98468 ↗
5. s5.s5 calc (↑k : ℝ) * (↑k : ℝ) ≤ (↑n : ℝ)
  Closes the goal.
  Lean, line 32
  _ ≤ (n : ℝ) := hnk
  targets/erdos-1094/nodes/erdos-1094--h3--h2--h1/attempts/20261018T193200Z-t1018-c-partial.lean, line 32 at 6ba7fea98468 ↗

import Mathlib
import Nodes.«erdos-1094--h3--h2--h1».Context

open scoped Nat

/-! Hole `h_ees` 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__h1 : ∃ (c : ℝ),
  (0 : ℝ) < c ∧
    ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := by
  -- approach: n ≥ k² is immediate with c ≤ 1/2; only the range n < k² needs EES
  -- licence: CC-BY-4.0
  -- label: EES bound below k squared
  -- claim: $\exists c>0\,\exists K\,\forall n,k:\ K<k,\ 2k\le n<k^2,\ \mathrm{lpf}\binom{n}{k}>k \Rightarrow k^{1+c}<n$
  -- The Ecklund–Erdős–Selfridge bound restricted to the only range where it has content.
  have h_lt : ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K : ℕ), ∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k →
      (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := sorry
  obtain ⟨c, hc, K, hK⟩ := h_lt
  refine ⟨min c (1 / 2), lt_min hc (by norm_num), K + 1, fun n k hk h2 hmf => ?_⟩
  have hk1 : (1 : ℝ) < (k : ℝ) := by exact_mod_cast (show 1 < k by omega)
  by_cases hn : n < k * k
  · calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + c) :=
          Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_left c (1 / 2)])
      _ < (n : ℝ) := hK n k (by omega) h2 hn hmf
  · replace hn := not_lt.mp hn
    have hnk : ((k : ℝ) * k) ≤ (n : ℝ) := by exact_mod_cast hn
    calc (k : ℝ) ^ ((1 : ℝ) + min c (1 / 2)) ≤ (k : ℝ) ^ ((1 : ℝ) + 1 / 2) :=
          Real.rpow_le_rpow_of_exponent_le hk1.le (by linarith [min_le_right c (1 / 2)])
      _ < (k : ℝ) ^ (2 : ℝ) := Real.rpow_lt_rpow_of_exponent_lt hk1 (by norm_num)
      _ = (k : ℝ) * k := by rw [Real.rpow_two, sq]
      _ ≤ (n : ℝ) := hnk

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).

How to read a statement’s page →