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

beyond van Doorn–Tang with n/gcd(n,k) prime

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

open

Hole h_gp of erdos-1094--h2--h2--h3 (split by 20261014T111449Z-t1014-y-partial.lean).

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

Only finitely many $k$ admit an $n$ with $n\ge k^3$ and $n+1>\exp\bigl((\log k)^2/(20\log\log k)\bigr)$ (natural logarithms, over the reals) such that $k\lfloor n/k\rfloor$ divides $k!$, the least prime factor of $\binom{n}{k}$ exceeds $\lfloor n/k\rfloor$, and $n/\gcd(n,k)$ is prime. Lean conventions: n / k is floor division, $n/\gcd(n,k)$ is natural-number division, exact here since the gcd divides $n$, Nat.minFac is the least prime factor (1 at 1, 2 at 0), and Real.log is 0 at 0, so for small $k$ the exponent is a junk value ($\log\log 1=0$ and division by 0 gives 0).

unverified · history

Lean

theorem erdos_1094__h2__h2__h3__h1 : ∃ (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 → Nat.Prime (n / n.gcd 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 20261015T144930Z-t1015c-a08-partial.lean (merged in a6465ef9ec4b, attestation 000545).

h_ndvd → erdos-1094--h2--h2--h3--h1--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},\ \ k\nmid n\ \Longrightarrow\ k\le K$

Read the partial proof (Lean)

theorem erdos_1094__h2__h2__h3__h1 : ∃ (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 → Nat.Prime (n / n.gcd k) → k ≤ K := by
  -- Proved here: if k ∣ n then gcd(n,k) = k, so p := n/k is prime with p ∣ k! (as p ∣ k*(n/k)),
  -- hence p ≤ k; but p = n/k ≥ k*k > k for k ≥ 2. So only k ∤ n remains open.
  have h_ndvd : ∃ (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 → Nat.Prime (n / n.gcd k) →
                ¬ k ∣ n → k ≤ K := by
    sorry
  obtain ⟨K, hK⟩ := h_ndvd
  refine ⟨max K 1, fun n k hk hn he hd hm hp => ?_⟩
  by_cases hkn : k ∣ n
  · rcases Nat.lt_or_ge k 2 with h1 | h2
    · exact le_trans (by omega) (le_max_right K 1)
    · exfalso
      have hg : n.gcd k = k := Nat.gcd_eq_right hkn
      rw [hg] at hp
      have hpk : n / k ∣ k.factorial := (Dvd.intro_left k rfl).trans hd
      have hle : n / k ≤ k := (Nat.Prime.dvd_factorial hp).1 hpk
      have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
      nlinarith
  · exact le_trans (hK n k hk hn he hd hm hp hkn) (le_max_left K 1)

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--h1/attempts/20261015T144930Z-t1015c-a08-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--h2--h2--h3--h1».Context

open scoped Nat

/-! Hole `h_gp` 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__h1 : ∃ (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 → Nat.Prime (n / n.gcd k) → k ≤ 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

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

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

Depends on (1), each in words

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

erdos-1094--h2--h2--h3--h1--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},\ \ k\nmid n\ \Longrightarrow\ k\le K$

Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000545.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--h1/Witness.lean, sha256 b811935b5326.

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

/-! The witness slot for a hole (D-29, F07-R6). Replace `sorry` with an instance
satisfying this statement's hypotheses; until then the node is blocked. -/

theorem witness : True := trivial

No gloss yet: no one has written in words what this witness says (D-3 v3.30); the Lean above is the witness. How to write one →

Attempts (2)

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

Untrusted contributor text — a partial assembly: it records an attempt, not a proof; its attestation names the file, and no hash in the record binds these bytes.

Untrusted: partial assembly (D-12 #5), by t1015c-a08; merged in a6465ef9ec4b under attestations/000545.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--h1/attempts/20261015T144930Z-t1015c-a08-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 20261015T144930Z-t1015c-a08-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_ndvd 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 ∣ n → 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 → Nat.Prime (n / n.gcd k) → k ≤ K, with h_ndvd : ∃ (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 ∣ n → k ≤ K.
Uses library Real.exp, Real.log, Nat.Prime.
Left open as a hole; its statement is erdos-1094--h2--h2--h3--h1--h1 (open).
Lean, lines 17–24
```
  have h_ndvd : ∃ (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 → Nat.Prime (n / n.gcd k) →
                ¬ k ∣ n → k ≤ K := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, lines 17–24 at 6ba7fea98468 ↗
s2 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 ∣ n → 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 → Nat.Prime (n / n.gcd 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 ∣ n → k ≤ K.
Lean, line 25
```
  obtain ⟨K, hK⟩ := h_ndvd
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, line 25 at 6ba7fea98468 ↗
s3 case
Leaves k ≤ max K (1 : ℕ), with hkn : k ∣ n.
Uses library Nat.lt_or_ge.
Lean, lines 28–36
```
  · rcases Nat.lt_or_ge k 2 with h1 | h2
    · exact le_trans (by omega) (le_max_right K 1)
    · exfalso
      have hg : n.gcd k = k := Nat.gcd_eq_right hkn
      rw [hg] at hp
      have hpk : n / k ∣ k.factorial := (Dvd.intro_left k rfl).trans hd
      have hle : n / k ≤ k := (Nat.Prime.dvd_factorial hp).1 hpk
      have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
      nlinarith
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, lines 28–36 at 6ba7fea98468 ↗
1. s3.s1 case
  Leaves k ≤ max K (1 : ℕ), with h1 : k < (2 : ℕ).
  Uses library le_trans, le_max_right.
  Lean, line 29
  · exact le_trans (by omega) (le_max_right K 1)
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, line 29 at 6ba7fea98468 ↗
2. s3.s2 case
  Leaves k ≤ max K (1 : ℕ), with h2 : k ≥ (2 : ℕ).
  Lean, lines 30–36
  · exfalso have hg : n.gcd k = k := Nat.gcd_eq_right hkn rw [hg] at hp have hpk : n / k ∣ k.factorial := (Dvd.intro_left k rfl).trans hd have hle : n / k ≤ k := (Nat.Prime.dvd_factorial hp).1 hpk have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn nlinarith
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, lines 30–36 at 6ba7fea98468 ↗
  s3.s2.hg have n.gcd k = k
  Leaves False, with hg : n.gcd k = k.
  Uses library Nat.gcd_eq_right.
  Lean, line 31
  have hg : n.gcd k = k := Nat.gcd_eq_right hkn
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, line 31 at 6ba7fea98468 ↗
  s3.s2.hpk have n / k ∣ k !
  Leaves False, with hpk : n / k ∣ k !.
  Uses library Dvd.intro_left, rfl.
  Lean, line 33
  have hpk : n / k ∣ k.factorial := (Dvd.intro_left k rfl).trans hd
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, line 33 at 6ba7fea98468 ↗
  s3.s2.hle have n / k ≤ k
  Leaves False, with hle : n / k ≤ k.
  Uses library Nat.Prime.dvd_factorial.
  Lean, line 34
  have hle : n / k ≤ k := (Nat.Prime.dvd_factorial hp).1 hpk
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, line 34 at 6ba7fea98468 ↗
  s3.s2.hkk have k * k ≤ n / k
  Leaves False, with hkk : k * k ≤ n / k.
  Uses library Nat.le_div_iff_mul_le.
  Lean, line 35
  have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
  targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, line 35 at 6ba7fea98468 ↗
s4 case
Leaves k ≤ max K (1 : ℕ), with hkn : ¬k ∣ n.
Uses library le_trans, le_max_left.
Lean, line 37
```
  · exact le_trans (hK n k hk hn he hd hm hp hkn) (le_max_left K 1)
```
targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1/attempts/20261015T144930Z-t1015c-a08-partial.lean, line 37 at 6ba7fea98468 ↗

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

open scoped Nat

/-! Hole `h_gp` 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__h1 : ∃ (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 → Nat.Prime (n / n.gcd k) → k ≤ K := by
  -- Proved here: if k ∣ n then gcd(n,k) = k, so p := n/k is prime with p ∣ k! (as p ∣ k*(n/k)),
  -- hence p ≤ k; but p = n/k ≥ k*k > k for k ≥ 2. So only k ∤ n remains open.
  have h_ndvd : ∃ (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 → Nat.Prime (n / n.gcd k) →
                ¬ k ∣ n → k ≤ K := by
    sorry
  obtain ⟨K, hK⟩ := h_ndvd
  refine ⟨max K 1, fun n k hk hn he hd hm hp => ?_⟩
  by_cases hkn : k ∣ n
  · rcases Nat.lt_or_ge k 2 with h1 | h2
    · exact le_trans (by omega) (le_max_right K 1)
    · exfalso
      have hg : n.gcd k = k := Nat.gcd_eq_right hkn
      rw [hg] at hp
      have hpk : n / k ∣ k.factorial := (Dvd.intro_left k rfl).trans hd
      have hle : n / k ≤ k := (Nat.Prime.dvd_factorial hp).1 hpk
      have hkk : k * k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
      nlinarith
  · exact le_trans (hK n k hk hn he hd hm hp hkn) (le_max_left K 1)

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 →