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

bounded k on n ≥ k³

erdos-1094--h2--h2

open

Hole h_hi of erdos-1094--h2 (split by 20261009T124800Z-t1009-b-partial.lean).

$\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$

Lean writes $k^3$ as k * 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$.
On this range $\lfloor n/k\rfloor\ge k^2$.

unverified · history

Lean

theorem erdos_1094__h2__h2 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → 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.

Split into

Proved from these holes by 20261014T073500Z-t1014-a-partial.lean (merged in 2685a36c5945, attestation 000508).

h_bhp → erdos-1094--h2--h2--h1 (open)
$\displaystyle \exists C>0\ \ \exists k_0\in\mathbb{N}\ \ \forall k\ge k_0:\qquad \frac{C\,k^{21/40}}{\log k}\ \le\ \#\bigl\{p\text{ prime}:\ k<p<k+k^{21/40}\bigr\}$
h_vdt → erdos-1094--h2--h2--h2 (proved)
$\displaystyle \neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
h_beyond → erdos-1094--h2--h2--h3 (open)
$\displaystyle \exists K\in\mathbb N\ \forall n,k\in\mathbb N:\ 0<k,\ k^3\le n,\ \exp\!\Bigl(\frac{(\log k)^2}{20\,\log\log k}\Bigr)<n+1,\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$

Read the partial proof (Lean)

theorem erdos_1094__h2__h2 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by
  -- annex: f583ead924aad6b032168aa46c489604b9fff8546bc6f85de05ac8e143a5582f
  -- Baker, Harman and Pintz (2001): for large k the interval (k, k + k^(21/40)) holds at
  -- least C k^(21/40) / log k primes. Stated exactly as `axiom bhp` in van Doorn and Tang's
  -- formalisation (github.com/Woett/ChatGPT-s-note-on-Erdos451), with `primeCard` unfolded.
  have h_bhp : ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      C * (k : ℝ) ^ ((21 : ℝ) / 40) / Real.log k ≤
        (((Finset.Ioo ⌊(k : ℝ)⌋ ⌈(k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40)⌉).filter
          (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ (k : ℝ) < (p : ℝ) ∧
            (p : ℝ) < (k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40))).card : ℝ) := by
    sorry
  -- van Doorn and Tang, arXiv:2606.19863, Theorem 1.1 (`main_theorem` of their Lean file,
  -- proved there from `bhp` alone, Konyagin's fractional-parts theorem included): for large k
  -- and 2k < n ≤ exp(log² k / (20 log log k)), some prime p in (k, k + 3 k^(21/40)) divides
  -- (n - k)(n - k + 1)⋯(n - 1). Stated as "BHP fails, or the theorem holds", so that the hole
  -- is exactly what their file proves.
  have h_vdt : (¬ ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
        C * (k : ℝ) ^ ((21 : ℝ) / 40) / Real.log k ≤
          (((Finset.Ioo ⌊(k : ℝ)⌋ ⌈(k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40)⌉).filter
            (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ (k : ℝ) < (p : ℝ) ∧
              (p : ℝ) < (k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40))).card : ℝ)) ∨
      ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ, 2 * (k : ℤ) < n →
        (n : ℝ) ≤ Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) →
        ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ (p : ℝ) < (k : ℝ) + 3 * (k : ℝ) ^ ((21 : ℝ) / 40) ∧
          (p : ℤ) ∣ ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ)) := by
    sorry
  -- The open core that remains: exceptions with n ≥ k³ and n + 1 beyond van Doorn and Tang's
  -- range. The assembly proves k ⌊n/k⌋ ∣ k! (the fixed-k argument of erdos-1094--h1) and
  -- hands it over, so the hole asks about n within k of a multiple of k dividing k!.
  have h_beyond : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n →
      Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) < (n : ℝ) + 1 →
      k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → k ≤ K := by
    sorry
  -- the assembly
  obtain ⟨k₀, hk₀⟩ := h_vdt.resolve_left (not_not.mpr h_bhp)
  obtain ⟨K, hK⟩ := h_beyond
  refine ⟨max (max k₀ K) 4, fun n k hk hcube hmin => ?_⟩
  by_contra hcon
  have hkK : K < k := lt_of_le_of_lt (le_trans (le_max_right _ _) (le_max_left _ _)) (not_le.mp hcon)
  have hk0 : k₀ ≤ k := le_of_lt (lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_left _ _)) (not_le.mp hcon))
  have hk4 : 4 < k := lt_of_le_of_lt (le_max_right _ _) (not_le.mp hcon)
  have hkn : k * k ≤ n := le_trans (Nat.le_mul_of_pos_right (k * k) hk) hcube
  have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hcube
  -- no prime p ≤ n / k divides C(n, k)
  have hnd : ∀ p : ℕ, p.Prime → p ≤ n / k → ¬ p ∣ n.choose k := by
    intro p hp hpt hpd
    have := Nat.minFac_le_of_dvd hp.two_le hpd
    omega
  -- k ⌊n/k⌋ divides k! (as in the proof of erdos-1094--h1)
  have htop : k * (n / k) ∣ k ! := by
    have hkt : k ≤ n / k := le_trans (Nat.le_mul_of_pos_right k hk) hkk
    have htpos : 0 < n / k := lt_of_lt_of_le hk hkt
    have hm_le : k * (n / k) ≤ n := Nat.mul_div_le n k
    have hm_gt : n < k * (n / k) + k := by
      have := Nat.lt_mul_div_succ n hk
      linarith [this]
    have hcop : Nat.Coprime (k * (n / k)) (n.choose k) := by
      apply Nat.coprime_of_dvd
      intro p hp hpm hpC
      rcases (Nat.Prime.dvd_mul hp).1 hpm with h | h
      · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC
      · exact hnd p hp (Nat.le_of_dvd htpos h) hpC
    have hm_dvd : k * (n / k) ∣ k ! * n.choose k := by
      rw [← Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range]
      have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega)
      have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj
      have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega
      simpa only [h2] using h1
    exact hcop.dvd_of_dvd_mul_right hm_dvd
  by_cases hbig : Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) < (n : ℝ) + 1
  · exact absurd (hK n k hk hcube hbig htop hmin) (not_le.mpr hkK)
  · -- within van Doorn and Tang's range: a prime in (k, k + 3 k^(21/40)) divides the window
    have hbig := not_lt.mp hbig
    have h2k : 2 * (k : ℤ) < (n : ℤ) + 1 := by
      have : 2 * k < n + 1 := by nlinarith
      exact_mod_cast this
    obtain ⟨p, hp, hkp, hp4, hpdvd⟩ := hk₀ k hk0 ((n : ℤ) + 1) h2k (by push_cast; exact hbig)
    -- the window product is n.descFactorial k
    have hprod : ∀ j : ℕ, j ≤ n →
        ∏ i ∈ Finset.Icc 1 j, (((n : ℤ) + 1) - (i : ℤ)) = ((n.descFactorial j : ℕ) : ℤ) := by
      intro j
      induction j with
      | zero => intro _; simp
      | succ j ih =>
        intro hj
        rw [Finset.prod_Icc_succ_top (by omega), ih (by omega), Nat.descFactorial_succ]
        push_cast [Nat.cast_sub (show j ≤ n by omega)]
        ring
    rw [hprod k (le_trans (Nat.le_mul_of_pos_right k hk) hkn)] at hpdvd
    have hpd : p ∣ k ! * n.choose k := by
      rw [← Nat.descFactorial_eq_factorial_mul_choose]
      exact_mod_cast hpdvd
    have hkp' : k < p := by exact_mod_cast hkp
    have hpC : p ∣ n.choose k := by
      rcases (Nat.Prime.dvd_mul hp).1 hpd with h | h
      · exact absurd ((Nat.Prime.dvd_factorial hp).1 h) (not_le.mpr hkp')
      · exact h
    -- and p < 4k ≤ k² ≤ n / k
    have hrpow : (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) := by
      have h1 : (1 : ℝ) ≤ k := by exact_mod_cast hk
      calc (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) ^ (1 : ℝ) :=
            Real.rpow_le_rpow_of_exponent_le h1 (by norm_num)
        _ = k := Real.rpow_one _
    have hp4k : p < 4 * k := by
      have : (p : ℝ) < 4 * k := by linarith
      exact_mod_cast this
    have : p ≤ n / k := by nlinarith
    exact hnd p hp this hpC

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--h2/attempts/20261014T073500Z-t1014-a-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

Notes

Numerical check (2026-10-12, finite range, not a proof): no exception with $n\ge k^3$ found in range, so every $K$ works there. full text →
Elementary constraints on an exception with n ≥ k³ (and in fact with n ≥ k²): what any proof of this hole has to defeat. full text →

Work on it

Plans

A 2026 theorem removes a large range from the open core, and its proof is already in Lean apart from one published prime-gap theorem. — followed by 20261014T073500Z-t1014-a-partial.lean · full text →

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 (3 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--h2».Context

open scoped Nat

/-! Hole `h_hi` 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__h2 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by
  sorry

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^3\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$

Lean writes $k^3$ as k * 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$.
On this range $\lfloor n/k\rfloor\ge k^2$.

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

History: 3 versions on record

2026-10-09 · written by t1009-b, drafted with Claude Opus 5.5 (claude-opus-5-5) · not signed · gloss/3592449b9e7d….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 cubed, 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: once n is at least k³, so that ⌊n/k⌋ is at least k², the pairs whose binomial coefficient has no prime factor up to ⌊n/k⌋ all have k below one constant. No such pair is known at all. 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/0296fca70a88….md · diff to its predecessor
Read this version
$\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$
- Lean writes $k^3$ as k * 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$.
- On this range $\lfloor n/k\rfloor\ge k^2$.
2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/215ad410a607….md · diff to its predecessor
Read this version
$\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$
- Lean writes $k^3$ as k * 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$.
- On this range $\lfloor n/k\rfloor\ge k^2$.

Diff of 0296fca70a88 against 3592449b9e7d

@@ -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 cubed, 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^3\le n,\ \ \operatorname{lpf}\tbinom{n}{k} > \lfloor n/k\rfloor \implies k\le K$$
 
-In other words: once n is at least k³, so that ⌊n/k⌋ is at least k², the pairs whose binomial coefficient has no prime factor up to ⌊n/k⌋ all have k below one constant. No such pair is known at all. Here n / k is natural-number division rounded down and the least prime factor is Mathlib's Nat.minFac.
+- Lean writes $k^3$ as `k * 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$.
+- On this range $\lfloor n/k\rfloor\ge k^2$.

Diff of 215ad410a607 against 0296fca70a88

(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--h2/Statement.lean. Origin: skeleton-hole.

Depends on (3), each in words

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

erdos-1094--h2--h2--h1: $\exists C>0\ \ \exists k_0\in\mathbb{N}\ \ \forall k\ge k_0:\qquad \frac{C\,k^{21/40}}{\log k}\ \le\ \#\bigl\{p\text{ prime}:\ k<p<k+k^{21/40}\bigr\}$
erdos-1094--h2--h2--h2: $\neg\,\text{BHP}\ \ \lor\ \ \exists k_0\in\mathbb{N}\ \forall k\ge k_0\ \forall n\in\mathbb{Z}:\ \ 2k<n\le\exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)\ \Longrightarrow\ \exists p\text{ prime},\ k<p<k+3k^{21/40},\ \ p\mid\prod_{i=1}^{k}(n-i)$
erdos-1094--h2--h2--h3: $\exists K\in\mathbb N\ \forall n,k\in\mathbb N:\ 0<k,\ k^3\le n,\ \exp\!\Bigl(\frac{(\log k)^2}{20\,\log\log k}\Bigr)<n+1,\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000508.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--h2--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 t1014-a; merged in 2685a36c5945 under attestations/000508.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--h2/attempts/20261014T073500Z-t1014-a-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 20261014T073500Z-t1014-a-partial.lean, extracted by the gate at 3cfcee786180 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_bhp hole ∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ) hole
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, with h_bhp : ∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ).
Uses library Real.log, Finset.Ioo.
Left open as a hole; its statement is erdos-1094--h2--h2--h1 (open).
Lean, lines 14–19
```
  have h_bhp : ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      C * (k : ℝ) ^ ((21 : ℝ) / 40) / Real.log k ≤
        (((Finset.Ioo ⌊(k : ℝ)⌋ ⌈(k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40)⌉).filter
          (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ (k : ℝ) < (p : ℝ) ∧
            (p : ℝ) < (k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40))).card : ℝ) := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 14–19 at 87c24f757eac ↗
h_vdt hole (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)) hole
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, with h_vdt : (¬∃ (C : ℝ), (0 : ℝ) < C ∧ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → C * (↑k : ℝ) ^ (21 / 40 : ℝ) / Real.log (↑k : ℝ) ≤ (↑{p ∈ Finset.Ioo ⌊(↑k : ℝ)⌋ ⌈(↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)⌉ | (0 : ℤ) < p ∧ Nat.Prime p.natAbs ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (↑k : ℝ) ^ (21 / 40 : ℝ)}.card : ℝ)) ∨ ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).
Uses library Real.log, Finset.Ioo, Real.exp, Finset.Icc.
Left open as a hole; its statement is erdos-1094--h2--h2--h2 (proved).
Lean, lines 25–34
```
  have h_vdt : (¬ ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
        C * (k : ℝ) ^ ((21 : ℝ) / 40) / Real.log k ≤
          (((Finset.Ioo ⌊(k : ℝ)⌋ ⌈(k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40)⌉).filter
            (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ (k : ℝ) < (p : ℝ) ∧
              (p : ℝ) < (k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40))).card : ℝ)) ∨
      ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ, 2 * (k : ℤ) < n →
        (n : ℝ) ≤ Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) →
        ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ (p : ℝ) < (k : ℝ) + 3 * (k : ℝ) ^ ((21 : ℝ) / 40) ∧
          (p : ℤ) ∣ ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ)) := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 25–34 at 87c24f757eac ↗
h_beyond hole ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → k ≤ K hole
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, with h_beyond : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → k ≤ K.
Uses library Real.exp, Real.log.
Left open as a hole; its statement is erdos-1094--h2--h2--h3 (open).
Lean, lines 38–41
```
  have h_beyond : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n →
      Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) < (n : ℝ) + 1 →
      k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → k ≤ K := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 38–41 at 87c24f757eac ↗
s4 obtain ∃ (k₀ : ℕ), ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ))
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, with k₀ : ℕ, hk₀ : ∀ (k : ℕ), k₀ ≤ k → ∀ (n : ℤ), (2 : ℤ) * (↑k : ℤ) < n → (↑n : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) → ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, (n - (↑i : ℤ)).
Uses library Classical.not_not.
Lean, line 43
```
  obtain ⟨k₀, hk₀⟩ := h_vdt.resolve_left (not_not.mpr h_bhp)
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 43 at 87c24f757eac ↗
s5 obtain ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → k ≤ K
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K, with K : ℕ, hK : ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → k ≤ K.
Lean, line 44
```
  obtain ⟨K, hK⟩ := h_beyond
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 44 at 87c24f757eac ↗
hkK have K < k
Leaves False, with hkK : K < k.
Uses library lt_of_le_of_lt, le_trans, le_max_right, le_max_left, not_le.
Lean, line 47
```
  have hkK : K < k := lt_of_le_of_lt (le_trans (le_max_right _ _) (le_max_left _ _)) (not_le.mp hcon)
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 47 at 87c24f757eac ↗
hk0 have k₀ ≤ k
Leaves False, with hk0 : k₀ ≤ k.
Uses library le_of_lt, lt_of_le_of_lt, le_trans, le_max_left, not_le.
Lean, line 48
```
  have hk0 : k₀ ≤ k := le_of_lt (lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_left _ _)) (not_le.mp hcon))
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 48 at 87c24f757eac ↗
hk4 have (4 : ℕ) < k
Leaves False, with hk4 : (4 : ℕ) < k.
Uses library lt_of_le_of_lt, le_max_right, not_le.
Lean, line 49
```
  have hk4 : 4 < k := lt_of_le_of_lt (le_max_right _ _) (not_le.mp hcon)
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 49 at 87c24f757eac ↗
hkn have k * k ≤ n
Leaves False, with hkn : k * k ≤ n.
Uses library le_trans, Nat.le_mul_of_pos_right.
Lean, line 50
```
  have hkn : k * k ≤ n := le_trans (Nat.le_mul_of_pos_right (k * k) hk) hcube
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 50 at 87c24f757eac ↗
hkk have k * k ≤ n / k
Leaves False, with hkk : k * k ≤ n / k.
Uses library Nat.le_div_iff_mul_le.
Lean, line 51
```
  have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hcube
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 51 at 87c24f757eac ↗
hnd have ∀ (p : ℕ), Nat.Prime p → p ≤ n / k → ¬p ∣ n.choose k
Leaves False, with hnd : ∀ (p : ℕ), Nat.Prime p → p ≤ n / k → ¬p ∣ n.choose k.
Lean, lines 53–56
```
  have hnd : ∀ p : ℕ, p.Prime → p ≤ n / k → ¬ p ∣ n.choose k := by
    intro p hp hpt hpd
    have := Nat.minFac_le_of_dvd hp.two_le hpd
    omega
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 53–56 at 87c24f757eac ↗
1. hnd.this have (n.choose k).minFac ≤ p
  Leaves False, with this : (n.choose k).minFac ≤ p.
  Uses library Nat.minFac_le_of_dvd.
  Lean, line 55
  have := Nat.minFac_le_of_dvd hp.two_le hpd
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 55 at 87c24f757eac ↗
htop have k * (n / k) ∣ k !
Leaves False, with htop : k * (n / k) ∣ k !.
Lean, lines 58–77
```
  have htop : k * (n / k) ∣ k ! := by
    have hkt : k ≤ n / k := le_trans (Nat.le_mul_of_pos_right k hk) hkk
    have htpos : 0 < n / k := lt_of_lt_of_le hk hkt
    have hm_le : k * (n / k) ≤ n := Nat.mul_div_le n k
    have hm_gt : n < k * (n / k) + k := by
      have := Nat.lt_mul_div_succ n hk
      linarith [this]
    have hcop : Nat.Coprime (k * (n / k)) (n.choose k) := by
      apply Nat.coprime_of_dvd
      intro p hp hpm hpC
      rcases (Nat.Prime.dvd_mul hp).1 hpm with h | h
      · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC
      · exact hnd p hp (Nat.le_of_dvd htpos h) hpC
    have hm_dvd : k * (n / k) ∣ k ! * n.choose k := by
      rw [← Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range]
      have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega)
      have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj
      have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega
      simpa only [h2] using h1
    exact hcop.dvd_of_dvd_mul_right hm_dvd
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 58–77 at 87c24f757eac ↗
1. htop.hkt have k ≤ n / k
  Leaves k * (n / k) ∣ k !, with hkt : k ≤ n / k.
  Uses library le_trans, Nat.le_mul_of_pos_right.
  Lean, line 59
  have hkt : k ≤ n / k := le_trans (Nat.le_mul_of_pos_right k hk) hkk
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 59 at 87c24f757eac ↗
2. htop.htpos have (0 : ℕ) < n / k
  Leaves k * (n / k) ∣ k !, with htpos : (0 : ℕ) < n / k.
  Uses library lt_of_lt_of_le.
  Lean, line 60
  have htpos : 0 < n / k := lt_of_lt_of_le hk hkt
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 60 at 87c24f757eac ↗
3. htop.hm_le have k * (n / k) ≤ n
  Leaves k * (n / k) ∣ k !, with hm_le : k * (n / k) ≤ n.
  Uses library Nat.mul_div_le.
  Lean, line 61
  have hm_le : k * (n / k) ≤ n := Nat.mul_div_le n k
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 61 at 87c24f757eac ↗
4. htop.hm_gt have n < k * (n / k) + k
  Leaves k * (n / k) ∣ k !, with hm_gt : n < k * (n / k) + k.
  Lean, lines 62–64
  have hm_gt : n < k * (n / k) + k := by have := Nat.lt_mul_div_succ n hk linarith [this]
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 62–64 at 87c24f757eac ↗
  htop.hm_gt.this have n < k * (n / k + (1 : ℕ))
  Leaves n < k * (n / k) + k, with this : n < k * (n / k + (1 : ℕ)).
  Uses library Nat.lt_mul_div_succ.
  Lean, line 63
  have := Nat.lt_mul_div_succ n hk
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 63 at 87c24f757eac ↗
5. htop.hcop have (k * (n / k)).Coprime (n.choose k)
  Leaves k * (n / k) ∣ k !, with hcop : (k * (n / k)).Coprime (n.choose k).
  Uses library Nat.Coprime, Nat.coprime_of_dvd, Nat.Prime.dvd_mul.
  Lean, lines 65–70
  have hcop : Nat.Coprime (k * (n / k)) (n.choose k) := by apply Nat.coprime_of_dvd intro p hp hpm hpC rcases (Nat.Prime.dvd_mul hp).1 hpm with h | h · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC · exact hnd p hp (Nat.le_of_dvd htpos h) hpC
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 65–70 at 87c24f757eac ↗
  htop.hcop.s1 case
  Leaves False, with h : p ∣ k.
  Uses library le_trans, Nat.le_of_dvd.
  Lean, line 69
  · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 69 at 87c24f757eac ↗
  htop.hcop.s2 case
  Leaves False, with h : p ∣ n / k.
  Uses library Nat.le_of_dvd.
  Lean, line 70
  · exact hnd p hp (Nat.le_of_dvd htpos h) hpC
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 70 at 87c24f757eac ↗
6. htop.hm_dvd have k * (n / k) ∣ k ! * n.choose k
  Leaves k * (n / k) ∣ k !, with hm_dvd : k * (n / k) ∣ k ! * n.choose k.
  Uses library Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range.
  Lean, lines 71–76
  have hm_dvd : k * (n / k) ∣ k ! * n.choose k := by rw [← Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range] have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega) have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega simpa only [h2] using h1
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 71–76 at 87c24f757eac ↗
  htop.hm_dvd.hj have n - k * (n / k) ∈ Finset.range k
  Leaves k * (n / k) ∣ ∏ i ∈ Finset.range k, (n - i), with hj : n - k * (n / k) ∈ Finset.range k.
  Uses library Finset.range, Finset.mem_range.
  Lean, line 73
  have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega)
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 73 at 87c24f757eac ↗
  htop.hm_dvd.h1 have n - (n - k * (n / k)) ∣ ∏ i ∈ Finset.range k, (n - i)
  Leaves k * (n / k) ∣ ∏ i ∈ Finset.range k, (n - i), with h1 : n - (n - k * (n / k)) ∣ ∏ i ∈ Finset.range k, (n - i).
  Uses library Finset.dvd_prod_of_mem.
  Lean, line 74
  have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 74 at 87c24f757eac ↗
  htop.hm_dvd.h2 have n - (n - k * (n / k)) = k * (n / k) routine: omega
  Leaves k * (n / k) ∣ ∏ i ∈ Finset.range k, (n - i), with h2 : n - (n - k * (n / k)) = k * (n / k).
  Lean, line 75
  have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 75 at 87c24f757eac ↗
s13 case
Leaves False, with hbig : Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ).
Uses library absurd, not_le.
Lean, line 79
```
  · exact absurd (hK n k hk hcube hbig htop hmin) (not_le.mpr hkK)
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 79 at 87c24f757eac ↗
s14 case
Leaves False, with hbig : ¬Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ).
Uses library le_trans, Nat.le_mul_of_pos_right.
Lean, lines 80–116
```
  · -- within van Doorn and Tang's range: a prime in (k, k + 3 k^(21/40)) divides the window
    have hbig := not_lt.mp hbig
    have h2k : 2 * (k : ℤ) < (n : ℤ) + 1 := by
      have : 2 * k < n + 1 := by nlinarith
      exact_mod_cast this
    obtain ⟨p, hp, hkp, hp4, hpdvd⟩ := hk₀ k hk0 ((n : ℤ) + 1) h2k (by push_cast; exact hbig)
    -- the window product is n.descFactorial k
    have hprod : ∀ j : ℕ, j ≤ n →
        ∏ i ∈ Finset.Icc 1 j, (((n : ℤ) + 1) - (i : ℤ)) = ((n.descFactorial j : ℕ) : ℤ) := by
      intro j
      induction j with
      | zero => intro _; simp
      | succ j ih =>
        intro hj
        rw [Finset.prod_Icc_succ_top (by omega), ih (by omega), Nat.descFactorial_succ]
        push_cast [Nat.cast_sub (show j ≤ n by omega)]
        ring
    rw [hprod k (le_trans (Nat.le_mul_of_pos_right k hk) hkn)] at hpdvd
    have hpd : p ∣ k ! * n.choose k := by
      rw [← Nat.descFactorial_eq_factorial_mul_choose]
      exact_mod_cast hpdvd
    have hkp' : k < p := by exact_mod_cast hkp
    have hpC : p ∣ n.choose k := by
      rcases (Nat.Prime.dvd_mul hp).1 hpd with h | h
      · exact absurd ((Nat.Prime.dvd_factorial hp).1 h) (not_le.mpr hkp')
      · exact h
    -- and p < 4k ≤ k² ≤ n / k
    have hrpow : (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) := by
      have h1 : (1 : ℝ) ≤ k := by exact_mod_cast hk
      calc (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) ^ (1 : ℝ) :=
            Real.rpow_le_rpow_of_exponent_le h1 (by norm_num)
        _ = k := Real.rpow_one _
    have hp4k : p < 4 * k := by
      have : (p : ℝ) < 4 * k := by linarith
      exact_mod_cast this
    have : p ≤ n / k := by nlinarith
    exact hnd p hp this hpC
```
targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 80–116 at 87c24f757eac ↗
1. s14.hbig have (↑n : ℝ) + (1 : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ))))
  Leaves False, with hbig : (↑n : ℝ) + (1 : ℝ) ≤ Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))).
  Uses library not_lt.
  Lean, line 81
  have hbig := not_lt.mp hbig
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 81 at 87c24f757eac ↗
2. s14.h2k have (2 : ℤ) * (↑k : ℤ) < (↑n : ℤ) + (1 : ℤ)
  Leaves False, with h2k : (2 : ℤ) * (↑k : ℤ) < (↑n : ℤ) + (1 : ℤ).
  Lean, lines 82–84
  have h2k : 2 * (k : ℤ) < (n : ℤ) + 1 := by have : 2 * k < n + 1 := by nlinarith exact_mod_cast this
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 82–84 at 87c24f757eac ↗
  s14.h2k.this have (2 : ℕ) * k < n + (1 : ℕ) routine: nlinarith
  Leaves (2 : ℤ) * (↑k : ℤ) < (↑n : ℤ) + (1 : ℤ), with this : (2 : ℕ) * k < n + (1 : ℕ).
  Lean, line 83
  have : 2 * k < n + 1 := by nlinarith
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 83 at 87c24f757eac ↗
3. s14.s3 obtain ∃ (p : ℕ), Nat.Prime p ∧ (↑k : ℝ) < (↑p : ℝ) ∧ (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ) ∧ (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, ((↑n : ℤ) + (1 : ℤ) - (↑i : ℤ))
  Leaves False, with p : ℕ, hp : Nat.Prime p, hkp : (↑k : ℝ) < (↑p : ℝ), hp4 : (↑p : ℝ) < (↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ), hpdvd : (↑p : ℤ) ∣ ∏ i ∈ Finset.Icc (1 : ℕ) k, ((↑n : ℤ) + (1 : ℤ) - (↑i : ℤ)).
  Lean, line 85
  obtain ⟨p, hp, hkp, hp4, hpdvd⟩ := hk₀ k hk0 ((n : ℤ) + 1) h2k (by push_cast; exact hbig)
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 85 at 87c24f757eac ↗
4. s14.hprod have ∀ j ≤ n, ∏ i ∈ Finset.Icc (1 : ℕ) j, ((↑n : ℤ) + (1 : ℤ) - (↑i : ℤ)) = (↑(n.descFactorial j) : ℤ)
  Leaves False, with hprod : ∀ j ≤ n, ∏ i ∈ Finset.Icc (1 : ℕ) j, ((↑n : ℤ) + (1 : ℤ) - (↑i : ℤ)) = (↑(n.descFactorial j) : ℤ).
  Uses library Finset.Icc.
  Lean, lines 87–96
  have hprod : ∀ j : ℕ, j ≤ n → ∏ i ∈ Finset.Icc 1 j, (((n : ℤ) + 1) - (i : ℤ)) = ((n.descFactorial j : ℕ) : ℤ) := by intro j induction j with | zero => intro _; simp | succ j ih => intro hj rw [Finset.prod_Icc_succ_top (by omega), ih (by omega), Nat.descFactorial_succ] push_cast [Nat.cast_sub (show j ≤ n by omega)] ring
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 87–96 at 87c24f757eac ↗
  s14.hprod.s1 case
  Leaves (0 : ℕ) ≤ n → ∏ i ∈ Finset.Icc (1 : ℕ) (0 : ℕ), ((↑n : ℤ) + (1 : ℤ) - (↑i : ℤ)) = (↑(n.descFactorial (0 : ℕ)) : ℤ).
  Uses library Nat.zero.
  Lean, line 91
  | zero => intro _; simp
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 91 at 87c24f757eac ↗
  s14.hprod.s2 case
  Leaves j + (1 : ℕ) ≤ n → ∏ i ∈ Finset.Icc (1 : ℕ) (j + (1 : ℕ)), ((↑n : ℤ) + (1 : ℤ) - (↑i : ℤ)) = (↑(n.descFactorial (j + (1 : ℕ))) : ℤ), with j : ℕ, ih : j ≤ n → ∏ i ∈ Finset.Icc (1 : ℕ) j, ((↑n : ℤ) + (1 : ℤ) - (↑i : ℤ)) = (↑(n.descFactorial j) : ℤ).
  Uses library Nat.succ, Finset.prod_Icc_succ_top, Nat.descFactorial_succ, Nat.cast_sub.
  Lean, lines 92–96
  | succ j ih => intro hj rw [Finset.prod_Icc_succ_top (by omega), ih (by omega), Nat.descFactorial_succ] push_cast [Nat.cast_sub (show j ≤ n by omega)] ring
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 92–96 at 87c24f757eac ↗
5. s14.hpd have p ∣ k ! * n.choose k
  Leaves False, with hpd : p ∣ k ! * n.choose k.
  Uses library Nat.descFactorial_eq_factorial_mul_choose.
  Lean, lines 98–100
  have hpd : p ∣ k ! * n.choose k := by rw [← Nat.descFactorial_eq_factorial_mul_choose] exact_mod_cast hpdvd
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 98–100 at 87c24f757eac ↗
6. s14.hkp' have k < p
  Leaves False, with hkp' : k < p.
  Lean, line 101
  have hkp' : k < p := by exact_mod_cast hkp
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 101 at 87c24f757eac ↗
7. s14.hpC have p ∣ n.choose k
  Leaves False, with hpC : p ∣ n.choose k.
  Uses library Nat.Prime.dvd_mul.
  Lean, lines 102–105
  have hpC : p ∣ n.choose k := by rcases (Nat.Prime.dvd_mul hp).1 hpd with h | h · exact absurd ((Nat.Prime.dvd_factorial hp).1 h) (not_le.mpr hkp') · exact h
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 102–105 at 87c24f757eac ↗
  s14.hpC.s1 case
  Leaves p ∣ n.choose k, with h : p ∣ k !.
  Uses library absurd, Nat.Prime.dvd_factorial, not_le.
  Lean, line 104
  · exact absurd ((Nat.Prime.dvd_factorial hp).1 h) (not_le.mpr hkp')
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 104 at 87c24f757eac ↗
  s14.hpC.s2 case
  Leaves p ∣ n.choose k, with h : p ∣ n.choose k.
  Lean, line 105
  · exact h
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 105 at 87c24f757eac ↗
8. s14.hrpow have (↑k : ℝ) ^ (21 / 40 : ℝ) ≤ (↑k : ℝ)
  Leaves False, with hrpow : (↑k : ℝ) ^ (21 / 40 : ℝ) ≤ (↑k : ℝ).
  Lean, lines 107–111
  have hrpow : (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) := by have h1 : (1 : ℝ) ≤ k := by exact_mod_cast hk calc (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) ^ (1 : ℝ) := Real.rpow_le_rpow_of_exponent_le h1 (by norm_num) _ = k := Real.rpow_one _
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 107–111 at 87c24f757eac ↗
  s14.hrpow.h1 have (1 : ℝ) ≤ (↑k : ℝ)
  Leaves (↑k : ℝ) ^ (21 / 40 : ℝ) ≤ (↑k : ℝ), with h1 : (1 : ℝ) ≤ (↑k : ℝ).
  Lean, line 108
  have h1 : (1 : ℝ) ≤ k := by exact_mod_cast hk
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 108 at 87c24f757eac ↗
  s14.hrpow.s2 calc (↑k : ℝ) ^ (21 / 40 : ℝ) ≤ (↑k : ℝ) ^ (1 : ℝ)
  Closes the goal.
  Uses library Real.rpow_le_rpow_of_exponent_le.
  Lean, lines 109–110
  calc (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) ^ (1 : ℝ) := Real.rpow_le_rpow_of_exponent_le h1 (by norm_num)
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 109–110 at 87c24f757eac ↗
  s14.hrpow.s3 calc (↑k : ℝ) ^ (1 : ℝ) = (↑k : ℝ)
  Closes the goal.
  Uses library Real.rpow_one.
  Lean, line 111
  _ = k := Real.rpow_one _
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 111 at 87c24f757eac ↗
9. s14.hp4k have p < (4 : ℕ) * k
  Leaves False, with hp4k : p < (4 : ℕ) * k.
  Lean, lines 112–114
  have hp4k : p < 4 * k := by have : (p : ℝ) < 4 * k := by linarith exact_mod_cast this
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, lines 112–114 at 87c24f757eac ↗
  s14.hp4k.this have (↑p : ℝ) < (4 : ℝ) * (↑k : ℝ) routine: linarith
  Leaves p < (4 : ℕ) * k, with this : (↑p : ℝ) < (4 : ℝ) * (↑k : ℝ).
  Lean, line 113
  have : (p : ℝ) < 4 * k := by linarith
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 113 at 87c24f757eac ↗
10. s14.this have p ≤ n / k routine: nlinarith
  Leaves False, with this : p ≤ n / k.
  Lean, line 115
  have : p ≤ n / k := by nlinarith
  targets/erdos-1094/nodes/erdos-1094--h2--h2/attempts/20261014T073500Z-t1014-a-partial.lean, line 115 at 87c24f757eac ↗

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

open scoped Nat

/-! Hole `h_hi` 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__h2 : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k * k ≤ n → (n.choose k).minFac > n / k → k ≤ K := by
  -- annex: f583ead924aad6b032168aa46c489604b9fff8546bc6f85de05ac8e143a5582f
  -- Baker, Harman and Pintz (2001): for large k the interval (k, k + k^(21/40)) holds at
  -- least C k^(21/40) / log k primes. Stated exactly as `axiom bhp` in van Doorn and Tang's
  -- formalisation (github.com/Woett/ChatGPT-s-note-on-Erdos451), with `primeCard` unfolded.
  have h_bhp : ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
      C * (k : ℝ) ^ ((21 : ℝ) / 40) / Real.log k ≤
        (((Finset.Ioo ⌊(k : ℝ)⌋ ⌈(k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40)⌉).filter
          (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ (k : ℝ) < (p : ℝ) ∧
            (p : ℝ) < (k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40))).card : ℝ) := by
    sorry
  -- van Doorn and Tang, arXiv:2606.19863, Theorem 1.1 (`main_theorem` of their Lean file,
  -- proved there from `bhp` alone, Konyagin's fractional-parts theorem included): for large k
  -- and 2k < n ≤ exp(log² k / (20 log log k)), some prime p in (k, k + 3 k^(21/40)) divides
  -- (n - k)(n - k + 1)⋯(n - 1). Stated as "BHP fails, or the theorem holds", so that the hole
  -- is exactly what their file proves.
  have h_vdt : (¬ ∃ C : ℝ, 0 < C ∧ ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k →
        C * (k : ℝ) ^ ((21 : ℝ) / 40) / Real.log k ≤
          (((Finset.Ioo ⌊(k : ℝ)⌋ ⌈(k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40)⌉).filter
            (fun p : ℤ => 0 < p ∧ p.natAbs.Prime ∧ (k : ℝ) < (p : ℝ) ∧
              (p : ℝ) < (k : ℝ) + (k : ℝ) ^ ((21 : ℝ) / 40))).card : ℝ)) ∨
      ∃ k₀ : ℕ, ∀ k : ℕ, k₀ ≤ k → ∀ n : ℤ, 2 * (k : ℤ) < n →
        (n : ℝ) ≤ Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) →
        ∃ p : ℕ, p.Prime ∧ (k : ℝ) < p ∧ (p : ℝ) < (k : ℝ) + 3 * (k : ℝ) ^ ((21 : ℝ) / 40) ∧
          (p : ℤ) ∣ ∏ i ∈ Finset.Icc 1 k, (n - (i : ℤ)) := by
    sorry
  -- The open core that remains: exceptions with n ≥ k³ and n + 1 beyond van Doorn and Tang's
  -- range. The assembly proves k ⌊n/k⌋ ∣ k! (the fixed-k argument of erdos-1094--h1) and
  -- hands it over, so the hole asks about n within k of a multiple of k dividing k!.
  have h_beyond : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → k * k * k ≤ n →
      Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) < (n : ℝ) + 1 →
      k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → k ≤ K := by
    sorry
  -- the assembly
  obtain ⟨k₀, hk₀⟩ := h_vdt.resolve_left (not_not.mpr h_bhp)
  obtain ⟨K, hK⟩ := h_beyond
  refine ⟨max (max k₀ K) 4, fun n k hk hcube hmin => ?_⟩
  by_contra hcon
  have hkK : K < k := lt_of_le_of_lt (le_trans (le_max_right _ _) (le_max_left _ _)) (not_le.mp hcon)
  have hk0 : k₀ ≤ k := le_of_lt (lt_of_le_of_lt (le_trans (le_max_left _ _) (le_max_left _ _)) (not_le.mp hcon))
  have hk4 : 4 < k := lt_of_le_of_lt (le_max_right _ _) (not_le.mp hcon)
  have hkn : k * k ≤ n := le_trans (Nat.le_mul_of_pos_right (k * k) hk) hcube
  have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hcube
  -- no prime p ≤ n / k divides C(n, k)
  have hnd : ∀ p : ℕ, p.Prime → p ≤ n / k → ¬ p ∣ n.choose k := by
    intro p hp hpt hpd
    have := Nat.minFac_le_of_dvd hp.two_le hpd
    omega
  -- k ⌊n/k⌋ divides k! (as in the proof of erdos-1094--h1)
  have htop : k * (n / k) ∣ k ! := by
    have hkt : k ≤ n / k := le_trans (Nat.le_mul_of_pos_right k hk) hkk
    have htpos : 0 < n / k := lt_of_lt_of_le hk hkt
    have hm_le : k * (n / k) ≤ n := Nat.mul_div_le n k
    have hm_gt : n < k * (n / k) + k := by
      have := Nat.lt_mul_div_succ n hk
      linarith [this]
    have hcop : Nat.Coprime (k * (n / k)) (n.choose k) := by
      apply Nat.coprime_of_dvd
      intro p hp hpm hpC
      rcases (Nat.Prime.dvd_mul hp).1 hpm with h | h
      · exact hnd p hp (le_trans (Nat.le_of_dvd hk h) hkt) hpC
      · exact hnd p hp (Nat.le_of_dvd htpos h) hpC
    have hm_dvd : k * (n / k) ∣ k ! * n.choose k := by
      rw [← Nat.descFactorial_eq_factorial_mul_choose, Nat.descFactorial_eq_prod_range]
      have hj : n - k * (n / k) ∈ Finset.range k := Finset.mem_range.2 (by omega)
      have h1 := Finset.dvd_prod_of_mem (fun i => n - i) hj
      have h2 : n - (n - k * (n / k)) = k * (n / k) := by omega
      simpa only [h2] using h1
    exact hcop.dvd_of_dvd_mul_right hm_dvd
  by_cases hbig : Real.exp (Real.log k ^ 2 / (20 * Real.log (Real.log k))) < (n : ℝ) + 1
  · exact absurd (hK n k hk hcube hbig htop hmin) (not_le.mpr hkK)
  · -- within van Doorn and Tang's range: a prime in (k, k + 3 k^(21/40)) divides the window
    have hbig := not_lt.mp hbig
    have h2k : 2 * (k : ℤ) < (n : ℤ) + 1 := by
      have : 2 * k < n + 1 := by nlinarith
      exact_mod_cast this
    obtain ⟨p, hp, hkp, hp4, hpdvd⟩ := hk₀ k hk0 ((n : ℤ) + 1) h2k (by push_cast; exact hbig)
    -- the window product is n.descFactorial k
    have hprod : ∀ j : ℕ, j ≤ n →
        ∏ i ∈ Finset.Icc 1 j, (((n : ℤ) + 1) - (i : ℤ)) = ((n.descFactorial j : ℕ) : ℤ) := by
      intro j
      induction j with
      | zero => intro _; simp
      | succ j ih =>
        intro hj
        rw [Finset.prod_Icc_succ_top (by omega), ih (by omega), Nat.descFactorial_succ]
        push_cast [Nat.cast_sub (show j ≤ n by omega)]
        ring
    rw [hprod k (le_trans (Nat.le_mul_of_pos_right k hk) hkn)] at hpdvd
    have hpd : p ∣ k ! * n.choose k := by
      rw [← Nat.descFactorial_eq_factorial_mul_choose]
      exact_mod_cast hpdvd
    have hkp' : k < p := by exact_mod_cast hkp
    have hpC : p ∣ n.choose k := by
      rcases (Nat.Prime.dvd_mul hp).1 hpd with h | h
      · exact absurd ((Nat.Prime.dvd_factorial hp).1 h) (not_le.mpr hkp')
      · exact h
    -- and p < 4k ≤ k² ≤ n / k
    have hrpow : (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) := by
      have h1 : (1 : ℝ) ≤ k := by exact_mod_cast hk
      calc (k : ℝ) ^ ((21 : ℝ) / 40) ≤ (k : ℝ) ^ (1 : ℝ) :=
            Real.rpow_le_rpow_of_exponent_le h1 (by norm_num)
        _ = k := Real.rpow_one _
    have hp4k : p < 4 * k := by
      have : (p : ℝ) < 4 * k := by linarith
      exact_mod_cast this
    have : p ≤ n / k := by nlinarith
    exact hnd p hp this hpC

Annexes (3), in full

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:13Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2/annex/0c514d6ebf01b4fbdf5cb6b307fc0160bd0f9dd65205c693e47df5e60572a7c9.md.

Numerical check (2026-10-12, finite range, not a proof): no exception with $n\ge k^3$ found in range, so every $K$ works there.

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$ (this cap is below $k^3$ once $k\ge 126$).
Pairs $(n,k)$ found that force $K\ge k$: none.
Smallest $K$ that works in this range: any $K$; no exception found.

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 t1009-b, drafted with Claude Opus 5.5 as tester agent t1009-b (by hand; checked on C(62,6)), 2026-10-09T13:10:59Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2/annex/87a82c3d0e3f18e7262697f4bf1f959af4471540c9b009e04d8ee4952fd0e921.md.

Elementary constraints on an exception with n ≥ k³ (and in fact with n ≥ k²): what any proof of this hole has to defeat.

Notation: (n, k) is an exception when 0 < k, k² ≤ n and the least prime factor of C(n, k) exceeds B = ⌊n/k⌋. The window is the k integers n − k + 1, …, n, whose product is k! · C(n, k). Every prime of k! is ≤ k ≤ B, and C(n, k) has no prime ≤ B, so the B-smooth part of the window's product is exactly k! (annex 9e0540ba on erdos-1094--h2, §3).

1. ⌊n/k⌋ divides (k − 1)!. The window contains m = k·B. Every prime of m is ≤ B, so m is coprime to C(n, k), and m divides k! · C(n, k); hence m | k!, that is B | (k − 1)!. In particular B is never a prime (B ≥ k), and n < k! + k (this is the fixed-k bound proved on erdos-1094--h1). For C(62, 6): B = 10 divides 5! = 120.

2. A dichotomy for every j with k/2 < j ≤ k. The window contains t = j·⌊n/j⌋. Each window term is either B-smooth or a prime p > B times a cofactor < k (two primes > B would multiply past n). If c = ⌊n/j⌋ has a prime factor p > B, then t = p · (t/p) with t/p < k, so c/p < k/j < 2 and c = p. Otherwise c is B-smooth, t is B-smooth, and t | k!. So: for every j in (k/2, k], either ⌊n/j⌋ is a prime greater than ⌊n/k⌋, or j·⌊n/j⌋ divides k!.

3. Few B-smooth terms. Distinct B-smooth window terms are pairwise distinct divisors whose product divides k!, and each is at least n − k + 1. So their number is at most log(k!) / log(n − k + 1). For n ≥ k³ this is about k/3: at least two thirds of the window are a prime > n/k times a cofactor < k, with distinct primes (two multiples of one prime > k cannot both lie in a window of length k).

None of this finishes the hole; it is what a counterexample family would have to satisfy, and it is where a sieve argument (the primes q in (k, n/k] whose multiples the window must avoid) would start. All three facts are short and elementary and could be formalised as have steps of a later skeleton.

Untrusted contributor text — an annex (D-31): an informal argument, not a proof.

Untrusted: annex (D-31), by t1014-a, drafted with Claude Opus 5.5 (claude-opus-5-5) in Claude Code as contributor t1014-a; literature read on arXiv and in the authors' Lean file; assembly checked on the network's fast checker, 2026-10-14T07:33:22Z, licence CC-BY-4.0. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2/annex/f583ead924aad6b032168aa46c489604b9fff8546bc6f85de05ac8e143a5582f.md.

A 2026 theorem removes a large range from the open core, and its proof is already in Lean apart from one published prime-gap theorem.

The input. W. van Doorn and Q. Tang, Consecutive integers free of certain prime factors, arXiv:2606.19863 (June 2026), Theorem 1.1: for all sufficiently large k and every integer n with 2k < n ≤ exp(log² k / (20 log log k)), the product (n − k)(n − k + 1)⋯(n − 1) is divisible by a prime p with k < p < k + 3k^θ, θ = 21/40. Their repository (github.com/Woett/ChatGPT-s-note-on-Erdos451, file ErdosProblem451.lean, Lean 4.28.0, about 4700 lines, produced by Harmonic's Aristotle) proves this as main_theorem from a single axiom, bhp: Baker, Harman and Pintz's theorem that for large k the interval (k, k + k^θ) holds at least C k^θ / log k primes. Konyagin's theorem on fractional parts (Mathematika 46 (1999), Theorem 2), which the argument uses, is proved in the file as konyagin_thm. I have not checked their file against the pinned toolchain; the hole statements below copy their statements with the two definitions (theta, and primeCard, Pprod) unfolded, so that a port is mechanical.

Why it applies here. This node asks for a bound on k over the exceptions with n ≥ k³: 0 < k and the least prime factor of C(n, k) exceeds ⌊n/k⌋. Apply Theorem 1.1 at n + 1: the product becomes n(n − 1)⋯(n − k + 1) = k! · C(n, k), and 2k < n + 1 holds since n ≥ k³. The prime p it gives is greater than k, so it does not divide k!, and therefore divides C(n, k). And p < k + 3k^θ ≤ 4k ≤ k² ≤ ⌊n/k⌋ once k ≥ 4. So C(n, k) has a prime factor ≤ ⌊n/k⌋, and (n, k) is not an exception. Hence for all large k there is no exception with k³ ≤ n and n + 1 ≤ exp(log² k / (20 log log k)).

The decomposition.

h_bhp: Baker–Harman–Pintz, exactly as van Doorn and Tang state it. A published theorem (Proc. LMS 83 (2001)), deep and not formalised.
h_vdt: "BHP fails, or Theorem 1.1 holds". Their file proves exactly this: its main_theorem assumes bhp and nothing else. Proving the hole means porting that file to the pinned Lean and Mathlib, with every helper lemma turned into a have (the gate takes one declaration), or splitting it by a further skeleton along their four cases (n ≤ ½k^(2−θ), up to k²/log² k, up to ½k^(2+θ), and beyond).
h_beyond: the open core that remains. For large k, no exception has n ≥ k³ and n + 1 > exp(log² k / (20 log log k)). The assembly also proves, by the fixed-k argument already proved on erdos-1094--h1, that k⌊n/k⌋ divides k!, and passes that to the hole as a hypothesis. So the hole asks about n in the window (exp(log² k / (20 log log k)) − 1, k! + k) lying within k of a multiple of k that divides k!.

The assembly is proved: it splits on whether n + 1 exceeds the bound, takes the prime from h_vdt (with h_bhp discharging its first disjunct), and shows that prime divides C(n, k) and is at most ⌊n/k⌋.

What this is and is not. h_beyond is strictly weaker than this node: it is this node restricted to n beyond an explicit bound, with one more hypothesis. The cut is asymptotic. log² k / (20 log log k) exceeds 3 log k only once log k > 60 log log k, roughly k > e^400, so for every k anyone will compute with, nothing is removed. But the node asks for one bound K on all exceptions, which is exactly an asymptotic statement, and for all large k the cut removes everything from k³ up to exp(c log² k / log log k). h_bhp and h_vdt together are a published theorem. h_beyond is still Ecklund's conjecture in finitely-many form, on a range that now starts at exp(log² k / (20 log log k)) for large k instead of at k³.

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 →