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

beyond van Doorn–Tang's range, n ≥ k³

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

open

Hole h_beyond of erdos-1094--h2--h2 (split by 20261014T073500Z-t1014-a-partial.lean).

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

In words: only finitely many $k$ admit an $n\ge k^3$ with $n+1>\exp(\log^2 k/(20\log\log k))$ (natural logarithms, over the reals) such that $k\cdot\lfloor n/k\rfloor$ divides $k!$ and the least prime factor of $\binom nk$ exceeds $\lfloor n/k\rfloor$.

Lean conventions: n / k is floor division; Real.log is 0 at 0 and takes $\log|x|$ for negative $x$, so for small $k$ the exponent is a junk value ($\log\log 1 = 0$ and division by 0 gives 0 in Lean); Nat.minFac is 1 at 1; 0 < k is a hypothesis.

unverified · history

Lean

theorem erdos_1094__h2__h2__h3 : ∃ (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.factorial → (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 this hole by 20261014T111449Z-t1014-y-partial.lean (merged in 8eb8acf03d74, attestation 000514).

h_gp → erdos-1094--h2--h2--h3--h1 (open)
$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 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}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime}\ \Longrightarrow\ k\le K$

Read the partial proof (Lean)

theorem erdos_1094__h2__h2__h3 : ∃ (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.factorial → (n.choose k).minFac > n / k → k ≤ K := by
  -- Proved here (assembly): under k*k ≤ n and minFac C(n,k) > n/k, the number n / gcd(n,k) is prime.
  -- Reason: n/gcd(n,k) divides C(n,k) (from k*C(n,k) = n*C(n-1,k-1) and coprimality), so all its
  -- prime factors exceed n/k ≥ k; a composite would be ≥ (n/k+1)^2 > n.
  have h_gcd_prime : ∀ (n k : ℕ), 0 < k → k * k ≤ n → (n.choose k).minFac > n / k →
      (n / n.gcd k).Prime := by
    intro n k hk hn hm
    have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn
    have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn
    have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
    set g := n.gcd k with hg
    have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
    have hgn : g ∣ n := Nat.gcd_dvd_left n k
    have hgk : g ∣ k := Nat.gcd_dvd_right n k
    -- k * C(n,k) = n * C(n-1,k-1)
    have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by
      have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
      rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
    have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
    have hdvd : n / g ∣ n.choose k := by
      have h1 : n / g ∣ n.choose k * (k / g) := by
        refine ⟨(n - 1).choose (k - 1), ?_⟩
        have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
        have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
        have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by
          rw [← e1, ← e2]; exact hid
        have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by
          linear_combination this
        exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
      exact hcop.dvd_of_dvd_mul_right h1
    have hCpos : 0 < n.choose k := Nat.choose_pos hkn
    -- n/g ≥ n/k ≥ k ≥ 1
    have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
    by_contra hnp
    have h2 : 2 ≤ n / g := by
      rcases Nat.lt_or_ge (n / g) 2 with h | h
      · -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n
        exfalso
        have hk1 : k ≤ 1 := by omega
        have hk1' : k = 1 := by omega
        subst hk1'
        have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega)
        have hn1 : n = 1 := by omega
        subst hn1
        simp at hm
      · exact h
    -- q := minFac (n/g); q ∣ C so minFac C ≤ q
    have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
    have hqC : (n.choose k).minFac ≤ (n / g).minFac :=
      Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
    have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp
    have hq : n / k + 1 ≤ (n / g).minFac := by omega
    have hng' : n / g ≤ n := Nat.div_le_self n g
    have hlt : n < (n / k + 1) * k := by
      have := Nat.lt_mul_div_succ n hk
      linarith [this]
    have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega)
    nlinarith
  -- The open half: the same statement, given in addition that n / gcd(n,k) is prime.
  have h_gp : ∃ (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.factorial → (n.choose k).minFac > n / k → (n / n.gcd k).Prime → k ≤ K := by
    sorry
  obtain ⟨K, hK⟩ := h_gp
  refine ⟨K, fun n k hk hn he hd hm => hK n k hk hn he hd hm ?_⟩
  exact h_gcd_prime n k hk (by nlinarith) hm

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--h3/attempts/20261014T111449Z-t1014-y-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 (2 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--h3».Context

open scoped Nat

/-! Hole `h_beyond` 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__h3 : ∃ (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.factorial → (n.choose k).minFac > n / k → k ≤ K := by
  sorry

In words, unverified — what this statement says; written by t1014-y, drafted with claude-opus-5-5 via Claude Code, 2026-10-14; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

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

History: 2 versions on record

2026-10-14 · written by t1014-y, drafted with claude-opus-5-5 via Claude Code · not signed · gloss/edf65ce8e981….md · the first version of its chain
Read this version
$\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.$

In words: only finitely many $k$ admit an $n\ge k^3$ with $n+1>\exp(\log^2 k/(20\log\log k))$ (natural logarithms, over the reals) such that $k\cdot\lfloor n/k\rfloor$ divides $k!$ and the least prime factor of $\binom nk$ exceeds $\lfloor n/k\rfloor$.

Lean conventions: n / k is floor division; Real.log is 0 at 0 and takes $\log|x|$ for negative $x$, so for small $k$ the exponent is a junk value ($\log\log 1 = 0$ and division by 0 gives 0 in Lean); Nat.minFac is 1 at 1; 0 < k is a hypothesis.
2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/33e7057d25b6….md · diff to its predecessor
Read this version
$\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.$

In words: only finitely many $k$ admit an $n\ge k^3$ with $n+1>\exp(\log^2 k/(20\log\log k))$ (natural logarithms, over the reals) such that $k\cdot\lfloor n/k\rfloor$ divides $k!$ and the least prime factor of $\binom nk$ exceeds $\lfloor n/k\rfloor$.

Lean conventions: n / k is floor division; Real.log is 0 at 0 and takes $\log|x|$ for negative $x$, so for small $k$ the exponent is a junk value ($\log\log 1 = 0$ and division by 0 gives 0 in Lean); Nat.minFac is 1 at 1; 0 < k is a hypothesis.

Diff of 33e7057d25b6 against edf65ce8e981

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

Depends on (1), each in words

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

erdos-1094--h2--h2--h3--h1: $\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 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}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime}\ \Longrightarrow\ k\le K$

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000514.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--h3/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-y; merged in 8eb8acf03d74 under attestations/000514.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--h3/attempts/20261014T111449Z-t1014-y-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 20261014T111449Z-t1014-y-partial.lean, extracted by the gate at f97b6921b55b 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_gcd_prime have ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k)
Leaves ∃ (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, with h_gcd_prime : ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k).
Lean, lines 18–71
```
  have h_gcd_prime : ∀ (n k : ℕ), 0 < k → k * k ≤ n → (n.choose k).minFac > n / k →
      (n / n.gcd k).Prime := by
    intro n k hk hn hm
    have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn
    have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn
    have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
    set g := n.gcd k with hg
    have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
    have hgn : g ∣ n := Nat.gcd_dvd_left n k
    have hgk : g ∣ k := Nat.gcd_dvd_right n k
    -- k * C(n,k) = n * C(n-1,k-1)
    have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by
      have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
      rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
    have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
    have hdvd : n / g ∣ n.choose k := by
      have h1 : n / g ∣ n.choose k * (k / g) := by
        refine ⟨(n - 1).choose (k - 1), ?_⟩
        have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
        have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
        have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by
          rw [← e1, ← e2]; exact hid
        have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by
          linear_combination this
        exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
      exact hcop.dvd_of_dvd_mul_right h1
    have hCpos : 0 < n.choose k := Nat.choose_pos hkn
    -- n/g ≥ n/k ≥ k ≥ 1
    have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
    by_contra hnp
    have h2 : 2 ≤ n / g := by
      rcases Nat.lt_or_ge (n / g) 2 with h | h
      · -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n
        exfalso
        have hk1 : k ≤ 1 := by omega
        have hk1' : k = 1 := by omega
        subst hk1'
        have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega)
        have hn1 : n = 1 := by omega
        subst hn1
        simp at hm
      · exact h
    -- q := minFac (n/g); q ∣ C so minFac C ≤ q
    have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
    have hqC : (n.choose k).minFac ≤ (n / g).minFac :=
      Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
    have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp
    have hq : n / k + 1 ≤ (n / g).minFac := by omega
    have hng' : n / g ≤ n := Nat.div_le_self n g
    have hlt : n < (n / k + 1) * k := by
      have := Nat.lt_mul_div_succ n hk
      linarith [this]
    have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega)
    nlinarith
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 18–71 at 6ba7fea98468 ↗
1. h_gcd_prime.hn0 have (0 : ℕ) < n
  Leaves Nat.Prime (n / n.gcd k), with hn0 : (0 : ℕ) < n.
  Uses library lt_of_lt_of_le, Nat.mul_pos.
  Lean, line 21
  have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 21 at 6ba7fea98468 ↗
2. h_gcd_prime.hkn have k ≤ n
  Leaves Nat.Prime (n / n.gcd k), with hkn : k ≤ n.
  Uses library le_trans, Nat.le_mul_of_pos_left.
  Lean, line 22
  have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 22 at 6ba7fea98468 ↗
3. h_gcd_prime.hkm have k ≤ n / k
  Leaves Nat.Prime (n / n.gcd k), with hkm : k ≤ n / k.
  Uses library Nat.le_div_iff_mul_le.
  Lean, line 23
  have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 23 at 6ba7fea98468 ↗
4. h_gcd_prime.hg0 have (0 : ℕ) < g
  Leaves Nat.Prime (n / g), with hg0 : (0 : ℕ) < g.
  Uses library Nat.gcd_pos_of_pos_left.
  Lean, line 25
  have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 25 at 6ba7fea98468 ↗
5. h_gcd_prime.hgn have g ∣ n
  Leaves Nat.Prime (n / g), with hgn : g ∣ n.
  Uses library Nat.gcd_dvd_left.
  Lean, line 26
  have hgn : g ∣ n := Nat.gcd_dvd_left n k
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 26 at 6ba7fea98468 ↗
6. h_gcd_prime.hgk have g ∣ k
  Leaves Nat.Prime (n / g), with hgk : g ∣ k.
  Uses library Nat.gcd_dvd_right.
  Lean, line 27
  have hgk : g ∣ k := Nat.gcd_dvd_right n k
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 27 at 6ba7fea98468 ↗
7. h_gcd_prime.hid have n * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * k
  Leaves Nat.Prime (n / g), with hid : n * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * k.
  Uses library Nat.sub_add_cancel.
  Lean, lines 29–31
  have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by have := Nat.add_one_mul_choose_eq (n - 1) (k - 1) rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 29–31 at 6ba7fea98468 ↗
  h_gcd_prime.hid.this have (n - (1 : ℕ) + (1 : ℕ)) * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = (n - (1 : ℕ) + (1 : ℕ)).choose (k - (1 : ℕ) + (1 : ℕ)) * (k - (1 : ℕ) + (1 : ℕ))
  Leaves n * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * k, with this : (n - (1 : ℕ) + (1 : ℕ)) * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = (n - (1 : ℕ) + (1 : ℕ)).choose (k - (1 : ℕ) + (1 : ℕ)) * (k - (1 : ℕ) + (1 : ℕ)).
  Uses library Nat.add_one_mul_choose_eq.
  Lean, line 30
  have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 30 at 6ba7fea98468 ↗
8. h_gcd_prime.hcop have (n / g).Coprime (k / g)
  Leaves Nat.Prime (n / g), with hcop : (n / g).Coprime (k / g).
  Uses library Nat.Coprime, Nat.coprime_div_gcd_div_gcd.
  Lean, line 32
  have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 32 at 6ba7fea98468 ↗
9. h_gcd_prime.hdvd have n / g ∣ n.choose k
  Leaves Nat.Prime (n / g), with hdvd : n / g ∣ n.choose k.
  Lean, lines 33–43
  have hdvd : n / g ∣ n.choose k := by have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm exact hcop.dvd_of_dvd_mul_right h1
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 33–43 at 6ba7fea98468 ↗
  h_gcd_prime.hdvd.h1 have n / g ∣ n.choose k * (k / g)
  Leaves n / g ∣ n.choose k, with h1 : n / g ∣ n.choose k * (k / g).
  Uses library Exists.intro, Nat.eq_of_mul_eq_mul_right.
  Lean, lines 34–42
  have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 34–42 at 6ba7fea98468 ↗
  h_gcd_prime.hdvd.h1.e1 have n = n / g * g
  Leaves n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), with e1 : n = n / g * g.
  Uses library Nat.div_mul_cancel.
  Lean, line 36
  have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 36 at 6ba7fea98468 ↗
  h_gcd_prime.hdvd.h1.e2 have k = k / g * g
  Leaves n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), with e2 : k = k / g * g.
  Uses library Nat.div_mul_cancel.
  Lean, line 37
  have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 37 at 6ba7fea98468 ↗
  h_gcd_prime.hdvd.h1.s3 have n / g * g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * (k / g * g)
  Leaves n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), with this : n / g * g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * (k / g * g).
  Lean, lines 38–39
  have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 38–39 at 6ba7fea98468 ↗
  h_gcd_prime.hdvd.h1.s4 have n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) * g = n.choose k * (k / g) * g
  Leaves n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), with this : n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) * g = n.choose k * (k / g) * g.
  Lean, lines 40–41
  have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 40–41 at 6ba7fea98468 ↗
10. h_gcd_prime.hCpos have (0 : ℕ) < n.choose k
  Leaves Nat.Prime (n / g), with hCpos : (0 : ℕ) < n.choose k.
  Uses library Nat.choose_pos.
  Lean, line 44
  have hCpos : 0 < n.choose k := Nat.choose_pos hkn
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 44 at 6ba7fea98468 ↗
11. h_gcd_prime.hng have n / k ≤ n / g
  Leaves Nat.Prime (n / g), with hng : n / k ≤ n / g.
  Uses library Nat.div_le_div_left, Nat.le_of_dvd.
  Lean, line 46
  have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 46 at 6ba7fea98468 ↗
12. h_gcd_prime.h2 have (2 : ℕ) ≤ n / g
  Leaves False, with h2 : (2 : ℕ) ≤ n / g.
  Uses library Nat.lt_or_ge.
  Lean, lines 48–59
  have h2 : 2 ≤ n / g := by rcases Nat.lt_or_ge (n / g) 2 with h | h · -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n exfalso have hk1 : k ≤ 1 := by omega have hk1' : k = 1 := by omega subst hk1' have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega) have hn1 : n = 1 := by omega subst hn1 simp at hm · exact h
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 48–59 at 6ba7fea98468 ↗
  h_gcd_prime.h2.s1 case
  Leaves (2 : ℕ) ≤ n / g, with h : n / g < (2 : ℕ).
  Lean, lines 50–58
  · -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n exfalso have hk1 : k ≤ 1 := by omega have hk1' : k = 1 := by omega subst hk1' have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega) have hn1 : n = 1 := by omega subst hn1 simp at hm
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 50–58 at 6ba7fea98468 ↗
  h_gcd_prime.h2.s1.hk1 have k ≤ (1 : ℕ) routine: omega
  Leaves False, with hk1 : k ≤ (1 : ℕ).
  Lean, line 52
  have hk1 : k ≤ 1 := by omega
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 52 at 6ba7fea98468 ↗
  h_gcd_prime.h2.s1.hk1' have k = (1 : ℕ) routine: omega
  Leaves False, with hk1' : k = (1 : ℕ).
  Lean, line 53
  have hk1' : k = 1 := by omega
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 53 at 6ba7fea98468 ↗
  h_gcd_prime.h2.s1.this have n ≤ (1 : ℕ)
  Leaves False, with this : n ≤ (1 : ℕ).
  Lean, line 55
  have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega)
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 55 at 6ba7fea98468 ↗
  h_gcd_prime.h2.s1.hn1 have n = (1 : ℕ) routine: omega
  Leaves False, with hn1 : n = (1 : ℕ).
  Lean, line 56
  have hn1 : n = 1 := by omega
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 56 at 6ba7fea98468 ↗
  h_gcd_prime.h2.s2 case
  Leaves (2 : ℕ) ≤ n / g, with h : n / g ≥ (2 : ℕ).
  Lean, line 59
  · exact h
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 59 at 6ba7fea98468 ↗
13. h_gcd_prime.hq2 have (2 : ℕ) ≤ (n / g).minFac
  Leaves False, with hq2 : (2 : ℕ) ≤ (n / g).minFac.
  Uses library Nat.minFac_prime.
  Lean, line 61
  have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 61 at 6ba7fea98468 ↗
14. h_gcd_prime.hqC have (n.choose k).minFac ≤ (n / g).minFac
  Leaves False, with hqC : (n.choose k).minFac ≤ (n / g).minFac.
  Uses library Nat.minFac_le_of_dvd, Nat.minFac_dvd.
  Lean, lines 62–63
  have hqC : (n.choose k).minFac ≤ (n / g).minFac := Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 62–63 at 6ba7fea98468 ↗
15. h_gcd_prime.hsq have (n / g).minFac ^ (2 : ℕ) ≤ n / g
  Leaves False, with hsq : (n / g).minFac ^ (2 : ℕ) ≤ n / g.
  Uses library Nat.minFac_sq_le_self.
  Lean, line 64
  have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 64 at 6ba7fea98468 ↗
16. h_gcd_prime.hq have n / k + (1 : ℕ) ≤ (n / g).minFac routine: omega
  Leaves False, with hq : n / k + (1 : ℕ) ≤ (n / g).minFac.
  Lean, line 65
  have hq : n / k + 1 ≤ (n / g).minFac := by omega
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 65 at 6ba7fea98468 ↗
17. h_gcd_prime.hng' have n / g ≤ n
  Leaves False, with hng' : n / g ≤ n.
  Uses library Nat.div_le_self.
  Lean, line 66
  have hng' : n / g ≤ n := Nat.div_le_self n g
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 66 at 6ba7fea98468 ↗
18. h_gcd_prime.hlt have n < (n / k + (1 : ℕ)) * k
  Leaves False, with hlt : n < (n / k + (1 : ℕ)) * k.
  Lean, lines 67–69
  have hlt : n < (n / k + 1) * k := by have := Nat.lt_mul_div_succ n hk linarith [this]
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 67–69 at 6ba7fea98468 ↗
  h_gcd_prime.hlt.this have n < k * (n / k + (1 : ℕ))
  Leaves n < (n / k + (1 : ℕ)) * k, with this : n < k * (n / k + (1 : ℕ)).
  Uses library Nat.lt_mul_div_succ.
  Lean, line 68
  have := Nat.lt_mul_div_succ n hk
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 68 at 6ba7fea98468 ↗
19. h_gcd_prime.this have (n / k + (1 : ℕ)) * k ≤ (n / k + (1 : ℕ)) * (n / k + (1 : ℕ))
  Leaves False, with this : (n / k + (1 : ℕ)) * k ≤ (n / k + (1 : ℕ)) * (n / k + (1 : ℕ)).
  Uses library Nat.mul_le_mul_left.
  Lean, line 70
  have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega)
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 70 at 6ba7fea98468 ↗
h_gp 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 → Nat.Prime (n / n.gcd k) → k ≤ K hole
Leaves ∃ (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, with h_gp : ∃ (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 → Nat.Prime (n / n.gcd k) → k ≤ K.
Uses library Real.exp, Real.log.
Left open as a hole; its statement is erdos-1094--h2--h2--h3--h1 (open).
Lean, lines 73–79
```
  have h_gp : ∃ (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.factorial → (n.choose k).minFac > n / k → (n / n.gcd k).Prime → k ≤ K := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 73–79 at 6ba7fea98468 ↗
s3 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 → Nat.Prime (n / n.gcd k) → k ≤ K
Leaves ∃ (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, 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 → Nat.Prime (n / n.gcd k) → k ≤ K.
Lean, line 80
```
  obtain ⟨K, hK⟩ := h_gp
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, line 80 at 6ba7fea98468 ↗
close term ∃ (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
Closes the goal.
Uses library Exists.intro.
Lean, lines 81–82
```
  refine ⟨K, fun n k hk hn he hd hm => hK n k hk hn he hd hm ?_⟩
  exact h_gcd_prime n k hk (by nlinarith) hm
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3/attempts/20261014T111449Z-t1014-y-partial.lean, lines 81–82 at 6ba7fea98468 ↗

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

open scoped Nat

/-! Hole `h_beyond` 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__h3 : ∃ (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.factorial → (n.choose k).minFac > n / k → k ≤ K := by
  -- Proved here (assembly): under k*k ≤ n and minFac C(n,k) > n/k, the number n / gcd(n,k) is prime.
  -- Reason: n/gcd(n,k) divides C(n,k) (from k*C(n,k) = n*C(n-1,k-1) and coprimality), so all its
  -- prime factors exceed n/k ≥ k; a composite would be ≥ (n/k+1)^2 > n.
  have h_gcd_prime : ∀ (n k : ℕ), 0 < k → k * k ≤ n → (n.choose k).minFac > n / k →
      (n / n.gcd k).Prime := by
    intro n k hk hn hm
    have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn
    have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn
    have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
    set g := n.gcd k with hg
    have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
    have hgn : g ∣ n := Nat.gcd_dvd_left n k
    have hgk : g ∣ k := Nat.gcd_dvd_right n k
    -- k * C(n,k) = n * C(n-1,k-1)
    have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by
      have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
      rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
    have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
    have hdvd : n / g ∣ n.choose k := by
      have h1 : n / g ∣ n.choose k * (k / g) := by
        refine ⟨(n - 1).choose (k - 1), ?_⟩
        have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
        have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
        have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by
          rw [← e1, ← e2]; exact hid
        have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by
          linear_combination this
        exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
      exact hcop.dvd_of_dvd_mul_right h1
    have hCpos : 0 < n.choose k := Nat.choose_pos hkn
    -- n/g ≥ n/k ≥ k ≥ 1
    have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
    by_contra hnp
    have h2 : 2 ≤ n / g := by
      rcases Nat.lt_or_ge (n / g) 2 with h | h
      · -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n
        exfalso
        have hk1 : k ≤ 1 := by omega
        have hk1' : k = 1 := by omega
        subst hk1'
        have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega)
        have hn1 : n = 1 := by omega
        subst hn1
        simp at hm
      · exact h
    -- q := minFac (n/g); q ∣ C so minFac C ≤ q
    have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
    have hqC : (n.choose k).minFac ≤ (n / g).minFac :=
      Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
    have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp
    have hq : n / k + 1 ≤ (n / g).minFac := by omega
    have hng' : n / g ≤ n := Nat.div_le_self n g
    have hlt : n < (n / k + 1) * k := by
      have := Nat.lt_mul_div_succ n hk
      linarith [this]
    have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega)
    nlinarith
  -- The open half: the same statement, given in addition that n / gcd(n,k) is prime.
  have h_gp : ∃ (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.factorial → (n.choose k).minFac > n / k → (n / n.gcd k).Prime → k ≤ K := by
    sorry
  obtain ⟨K, hK⟩ := h_gp
  refine ⟨K, fun n k hk hn he hd hm => hK n k hk hn he hd hm ?_⟩
  exact h_gcd_prime n k hk (by nlinarith) hm

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 →