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

ELS lower bound: k² ≤ C·n·log₂k when lpf C(n,k) > k

erdos-1094--h3--h2

open

Hole h_els of erdos-1094--h3 (split by 20261015T125200Z-t1015b-g-partial.lean).

$\displaystyle \exists C, K_1\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n,\ \ \operatorname{minFac}\tbinom{n}{k}>k \implies k^2 \le C\cdot n\cdot\lfloor\log_2 k\rfloor$

There are constants $C$ and $K_1$ such that for all $k>K_1$ and $n\ge 2k$, if every prime factor of $\binom{n}{k}$ exceeds $k$ then $k^2\le C\,n\lfloor\log_2 k\rfloor$; in words, $n\gg k^2/\log k$ on the pairs in question. $\operatorname{minFac}$ is Mathlib's Nat.minFac, the least prime factor (here $\binom{n}{k}\ge 2$); 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, and $k^2$ is k * k.

unverified · history

Lean

theorem erdos_1094__h3__h2 : ∃ (C : ℕ) (K₁ : ℕ),
  ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) 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.

Split into

Proved from these holes by 20261015T132800Z-t1015b-h-partial.lean (merged in ce10304b0c25, attestation 000543).

h_ees → erdos-1094--h3--h2--h1 (open)
$\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$
h_caseB → erdos-1094--h3--h2--h2 (open)
$\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}$
h_caseA → erdos-1094--h3--h2--h3 (open)
$\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}$

Read the partial proof (Lean)

theorem erdos_1094__h3__h2 : ∃ (C : ℕ) (K₁ : ℕ),
  ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) := by
  -- Partial proof along Erdős–Lacampagne–Selfridge, "Estimates of the least prime factor of a
  -- binomial coefficient", Math. Comp. 61 (1993) 215–224, Theorem 1 (p. 216) and its proof
  -- (pp. 216–218). ELS write N = n + k for the top; our n is their N. Three ranges:
  -- h_ees: N ≤ k^{1+c}. ELS p. 216: "It was shown in [1] that there is an absolute constant c > 0
  -- for which g(k) > k^{1+c}" — Ecklund, Erdős, Selfridge, "A new function associated with the
  -- prime factors of (n k)", Math. Comp. 28 (1974). Cited by ELS, not proved there.
  have h_ees : ∃ c : ℝ, 0 < c ∧ ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n →
      (n.choose k).minFac > k → (k : ℝ) ^ (1 + c) < (n : ℝ) := by
    sorry
  -- h_caseB: k^{1+c} < N < k^{7/4} (ELS p. 217, "Now only the case k^{1+c} < n + k < k^{7/4}
  -- remains"): some prime p in (k/2, k/2 + k^{7/8}) has two multiples in (N − k, N], hence
  -- divides C(N, k); proof counts the 'unusable' primes against Ingham's count of primes in
  -- (k/2, k/2 + k^{7/8}). The argument needs only N > 2k + 6k^{7/8}, so it holds for every c > 0.
  have h_caseB : ∀ c : ℝ, 0 < c → ∃ K₃ : ℕ, ∀ n k : ℕ, K₃ < k → (k : ℝ) ^ (1 + c) < (n : ℝ) →
      (n : ℝ) < (k : ℝ) ^ ((7 : ℝ) / 4) →
      ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    sorry
  -- h_caseA: k^{7/4} ≤ N < c₁k²/ln k (ELS pp. 216–217, inequalities (1)–(4)): Ingham gives two
  -- primes k/2 < p₁ < p₂ < p₁ + c₂ ln k < k/2 + k^{3/4}; one of them has two multiples in
  -- (N − k, N], hence divides C(N, k). Here c₁k²/ln k is written k² > C·N·log₂ k (C = ⌈ln 2 / c₁⌉).
  have h_caseA : ∃ C K₄ : ℕ, ∀ n k : ℕ, K₄ < k → (k : ℝ) ^ ((7 : ℝ) / 4) ≤ (n : ℝ) →
      C * (n * Nat.log 2 k) < k * k →
      ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    sorry
  -- Assembly: the three ranges cover every good N; a prime p < k dividing C(N, k) contradicts
  -- least prime factor > k.
  obtain ⟨c, hc, K₂, hE⟩ := h_ees
  obtain ⟨K₃, hB⟩ := h_caseB c hc
  obtain ⟨C, K₄, hA⟩ := h_caseA
  refine ⟨C, max K₂ (max K₃ K₄), fun n k hk h2k hmin => ?_⟩
  have hk2 : K₂ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hk3 : K₃ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
  have hk4 : K₄ < k := lt_of_le_of_lt (le_trans (le_max_right _ _) (le_max_right _ _)) hk
  by_contra hlt
  push_neg at hlt
  have he := hE n k hk2 h2k hmin
  have key : ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    rcases lt_or_ge (n : ℝ) ((k : ℝ) ^ ((7 : ℝ) / 4)) with h | h
    · exact hB n k hk3 he h
    · exact hA n k hk4 h hlt
  obtain ⟨p, hp, _, hpk, hd⟩ := key
  have hle := Nat.minFac_le_of_dvd hp.two_le hd
  omega

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/attempts/20261015T132800Z-t1015b-h-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

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

open scoped Nat

/-! Hole `h_els` 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 : ∃ (C : ℕ) (K₁ : ℕ),
  ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) := 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, K_1\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad K_1<k,\ \ 2k\le n,\ \ \operatorname{minFac}\tbinom{n}{k}>k \implies k^2 \le C\cdot n\cdot\lfloor\log_2 k\rfloor$

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

Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2/Statement.lean. Origin: skeleton-hole.

Depends on (3), each in words

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

erdos-1094--h3--h2--h1: $\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$
erdos-1094--h3--h2--h2: $\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}$
erdos-1094--h3--h2--h3: $\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}$

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000543.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/Witness.lean, sha256 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 t1015b-h; merged in ce10304b0c25 under attestations/000543.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/attempts/20261015T132800Z-t1015b-h-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 20261015T132800Z-t1015b-h-partial.lean, extracted by the gate at fa0a13ba270d 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_ees hole ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) hole
Leaves ∃ (C : ℕ) (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k), with h_ees : ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ).
Left open as a hole; its statement is erdos-1094--h3--h2--h1 (open).
Lean, lines 17–19
```
  have h_ees : ∃ c : ℝ, 0 < c ∧ ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n →
      (n.choose k).minFac > k → (k : ℝ) ^ (1 + c) < (n : ℝ) := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, lines 17–19 at 87c24f757eac ↗
h_caseB hole ∀ (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 hole
Leaves ∃ (C : ℕ) (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k), with h_caseB : ∀ (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.
Left open as a hole; its statement is erdos-1094--h3--h2--h2 (open).
Lean, lines 24–27
```
  have h_caseB : ∀ c : ℝ, 0 < c → ∃ K₃ : ℕ, ∀ n k : ℕ, K₃ < k → (k : ℝ) ^ (1 + c) < (n : ℝ) →
      (n : ℝ) < (k : ℝ) ^ ((7 : ℝ) / 4) →
      ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, lines 24–27 at 87c24f757eac ↗
h_caseA hole ∃ (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 hole
Leaves ∃ (C : ℕ) (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k), with h_caseA : ∃ (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.
Uses library Nat.log.
Left open as a hole; its statement is erdos-1094--h3--h2--h3 (open).
Lean, lines 31–34
```
  have h_caseA : ∃ C K₄ : ℕ, ∀ n k : ℕ, K₄ < k → (k : ℝ) ^ ((7 : ℝ) / 4) ≤ (n : ℝ) →
      C * (n * Nat.log 2 k) < k * k →
      ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, lines 31–34 at 87c24f757eac ↗
s4 obtain ∃ (c : ℝ), (0 : ℝ) < c ∧ ∃ (K₂ : ℕ), ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ)
Leaves ∃ (C : ℕ) (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k), with c : ℝ, hc : (0 : ℝ) < c, K₂ : ℕ, hE : ∀ (n k : ℕ), K₂ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ).
Lean, line 37
```
  obtain ⟨c, hc, K₂, hE⟩ := h_ees
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 37 at 87c24f757eac ↗
s5 obtain ∃ (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
Leaves ∃ (C : ℕ) (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k), with K₃ : ℕ, hB : ∀ (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.
Lean, line 38
```
  obtain ⟨K₃, hB⟩ := h_caseB c hc
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 38 at 87c24f757eac ↗
s6 obtain ∃ (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
Leaves ∃ (C : ℕ) (K₁ : ℕ), ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k), with C : ℕ, K₄ : ℕ, hA : ∀ (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.
Lean, line 39
```
  obtain ⟨C, K₄, hA⟩ := h_caseA
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 39 at 87c24f757eac ↗
hk2 have K₂ < k
Leaves k * k ≤ C * (n * Nat.log (2 : ℕ) k), with hk2 : K₂ < k.
Uses library lt_of_le_of_lt, le_max_left.
Lean, line 41
```
  have hk2 : K₂ < k := lt_of_le_of_lt (le_max_left _ _) hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 41 at 87c24f757eac ↗
hk3 have K₃ < k
Leaves k * k ≤ C * (n * Nat.log (2 : ℕ) k), with hk3 : K₃ < k.
Uses library lt_of_le_of_lt, le_trans, le_max_left, le_max_right.
Lean, line 42
```
  have hk3 : K₃ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 42 at 87c24f757eac ↗
hk4 have K₄ < k
Leaves k * k ≤ C * (n * Nat.log (2 : ℕ) k), with hk4 : K₄ < k.
Uses library lt_of_le_of_lt, le_trans, le_max_right.
Lean, line 43
```
  have hk4 : K₄ < k := lt_of_le_of_lt (le_trans (le_max_right _ _) (le_max_right _ _)) hk
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 43 at 87c24f757eac ↗
he have (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ)
Leaves False, with he : (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ).
Lean, line 46
```
  have he := hE n k hk2 h2k hmin
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 46 at 87c24f757eac ↗
key have ∃ (p : ℕ), Nat.Prime p ∧ k < (2 : ℕ) * p ∧ p < k ∧ p ∣ n.choose k
Leaves False, with key : ∃ (p : ℕ), Nat.Prime p ∧ k < (2 : ℕ) * p ∧ p < k ∧ p ∣ n.choose k.
Uses library lt_or_ge.
Lean, lines 47–50
```
  have key : ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    rcases lt_or_ge (n : ℝ) ((k : ℝ) ^ ((7 : ℝ) / 4)) with h | h
    · exact hB n k hk3 he h
    · exact hA n k hk4 h hlt
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, lines 47–50 at 87c24f757eac ↗
1. key.s1 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ k < (2 : ℕ) * p ∧ p < k ∧ p ∣ n.choose k, with h : (↑n : ℝ) < (↑k : ℝ) ^ (7 / 4 : ℝ).
  Lean, line 49
  · exact hB n k hk3 he h
  targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 49 at 87c24f757eac ↗
2. key.s2 case
  Leaves ∃ (p : ℕ), Nat.Prime p ∧ k < (2 : ℕ) * p ∧ p < k ∧ p ∣ n.choose k, with h : (↑k : ℝ) ^ (7 / 4 : ℝ) ≤ (↑n : ℝ).
  Lean, line 50
  · exact hA n k hk4 h hlt
  targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 50 at 87c24f757eac ↗
s12 obtain ∃ (p : ℕ), Nat.Prime p ∧ k < (2 : ℕ) * p ∧ p < k ∧ p ∣ n.choose k
Leaves False, with p : ℕ, hp : Nat.Prime p, left✝ : k < (2 : ℕ) * p, hpk : p < k, hd : p ∣ n.choose k.
Lean, line 51
```
  obtain ⟨p, hp, _, hpk, hd⟩ := key
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 51 at 87c24f757eac ↗
hle have (n.choose k).minFac ≤ p
Leaves False, with hle : (n.choose k).minFac ≤ p.
Uses library Nat.minFac_le_of_dvd.
Lean, line 52
```
  have hle := Nat.minFac_le_of_dvd hp.two_le hd
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 52 at 87c24f757eac ↗
close term False routine: omega
Closes the goal.
Lean, line 53
```
  omega
```
targets/erdos-1094/nodes/erdos-1094--h3--h2/attempts/20261015T132800Z-t1015b-h-partial.lean, line 53 at 87c24f757eac ↗

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

open scoped Nat

/-! Hole `h_els` 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 : ∃ (C : ℕ) (K₁ : ℕ),
  ∀ (n k : ℕ), K₁ < k → (2 : ℕ) * k ≤ n → (n.choose k).minFac > k → k * k ≤ C * (n * Nat.log (2 : ℕ) k) := by
  -- Partial proof along Erdős–Lacampagne–Selfridge, "Estimates of the least prime factor of a
  -- binomial coefficient", Math. Comp. 61 (1993) 215–224, Theorem 1 (p. 216) and its proof
  -- (pp. 216–218). ELS write N = n + k for the top; our n is their N. Three ranges:
  -- h_ees: N ≤ k^{1+c}. ELS p. 216: "It was shown in [1] that there is an absolute constant c > 0
  -- for which g(k) > k^{1+c}" — Ecklund, Erdős, Selfridge, "A new function associated with the
  -- prime factors of (n k)", Math. Comp. 28 (1974). Cited by ELS, not proved there.
  have h_ees : ∃ c : ℝ, 0 < c ∧ ∃ K₂ : ℕ, ∀ n k : ℕ, K₂ < k → 2 * k ≤ n →
      (n.choose k).minFac > k → (k : ℝ) ^ (1 + c) < (n : ℝ) := by
    sorry
  -- h_caseB: k^{1+c} < N < k^{7/4} (ELS p. 217, "Now only the case k^{1+c} < n + k < k^{7/4}
  -- remains"): some prime p in (k/2, k/2 + k^{7/8}) has two multiples in (N − k, N], hence
  -- divides C(N, k); proof counts the 'unusable' primes against Ingham's count of primes in
  -- (k/2, k/2 + k^{7/8}). The argument needs only N > 2k + 6k^{7/8}, so it holds for every c > 0.
  have h_caseB : ∀ c : ℝ, 0 < c → ∃ K₃ : ℕ, ∀ n k : ℕ, K₃ < k → (k : ℝ) ^ (1 + c) < (n : ℝ) →
      (n : ℝ) < (k : ℝ) ^ ((7 : ℝ) / 4) →
      ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    sorry
  -- h_caseA: k^{7/4} ≤ N < c₁k²/ln k (ELS pp. 216–217, inequalities (1)–(4)): Ingham gives two
  -- primes k/2 < p₁ < p₂ < p₁ + c₂ ln k < k/2 + k^{3/4}; one of them has two multiples in
  -- (N − k, N], hence divides C(N, k). Here c₁k²/ln k is written k² > C·N·log₂ k (C = ⌈ln 2 / c₁⌉).
  have h_caseA : ∃ C K₄ : ℕ, ∀ n k : ℕ, K₄ < k → (k : ℝ) ^ ((7 : ℝ) / 4) ≤ (n : ℝ) →
      C * (n * Nat.log 2 k) < k * k →
      ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    sorry
  -- Assembly: the three ranges cover every good N; a prime p < k dividing C(N, k) contradicts
  -- least prime factor > k.
  obtain ⟨c, hc, K₂, hE⟩ := h_ees
  obtain ⟨K₃, hB⟩ := h_caseB c hc
  obtain ⟨C, K₄, hA⟩ := h_caseA
  refine ⟨C, max K₂ (max K₃ K₄), fun n k hk h2k hmin => ?_⟩
  have hk2 : K₂ < k := lt_of_le_of_lt (le_max_left _ _) hk
  have hk3 : K₃ < k := lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_right _ _)) hk
  have hk4 : K₄ < k := lt_of_le_of_lt (le_trans (le_max_right _ _) (le_max_right _ _)) hk
  by_contra hlt
  push_neg at hlt
  have he := hE n k hk2 h2k hmin
  have key : ∃ p : ℕ, p.Prime ∧ k < 2 * p ∧ p < k ∧ p ∣ n.choose k := by
    rcases lt_or_ge (n : ℝ) ((k : ℝ) ^ ((7 : ℝ) / 4)) with h | h
    · exact hB n k hk3 he h
    · exact hA n k hk4 h hlt
  obtain ⟨p, hp, _, hpk, hd⟩ := key
  have hle := Nat.minFac_le_of_dvd hp.two_le hd
  omega

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 →