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

2k ≤ n < k³ with n/gcd(n,k) free of primes ≤ k

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

open

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

$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^3,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$

Only finitely many $k$ admit an $n$ with $2k\le n<k^3$ such that neither the binomial coefficient $\binom{n}{k}$ nor the cofactor $n/\gcd(n,k)$ has a prime factor at most $k$. Lean writes $k^3$ as k * k * k; Nat.minFac is the least prime factor (1 at 1, 2 at 0); $n/\gcd(n,k)$ is natural-number division, exact here since the gcd divides $n$.

unverified · history

Lean

theorem erdos_1094__h2__h1__h1__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > 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 20261015T151456Z-t1015c-a06-partial.lean (merged in 52dcd39070e7, attestation 000558).

h_low → erdos-1094--h2--h1--h1--h1--h1 (open)
$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^2,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$
h_high → erdos-1094--h2--h1--h1--h1--h2 (open)
$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n<k^3,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$

Read the partial proof (Lean)

theorem erdos_1094__h2__h1__h1__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
  -- Split the range 2k ≤ n < k³ at n = k²: the lower band (n < k², Sylvester–Schur/Ecklund
  -- regime) and the upper band (k² ≤ n < k³). Each hole carries a stronger hypothesis.
  have h_low : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k →
      (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
    sorry
  have h_high : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k →
      (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
    sorry
  obtain ⟨K1, hK1⟩ := h_low
  obtain ⟨K2, hK2⟩ := h_high
  refine ⟨max K1 K2, fun n k hk hn hn3 hc hg => ?_⟩
  rcases lt_or_ge n (k * k) with h | h
  · exact le_max_of_le_left (hK1 n k hk hn h hc hg)
  · exact le_max_of_le_right (hK2 n k hk h hn3 hc hg)

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--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-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--h1--h1--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__h1__h1__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > 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/fcbbebbd5ff2….md · Improve these words →

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

Depends on (2), each in words

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

erdos-1094--h2--h1--h1--h1--h1: $\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ 2k\le n<k^2,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$
erdos-1094--h2--h1--h1--h1--h2: $\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n<k^3,\ \ \operatorname{minFac}\tbinom{n}{k}>k,\ \ \operatorname{minFac}\!\Bigl(\frac{n}{\gcd(n,k)}\Bigr)>k\ \Longrightarrow\ k\le K$

Attestation: none of a proof

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

import Mathlib
import Nodes.«erdos-1094--h2--h1--h1--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-a06; merged in 52dcd39070e7 under attestations/000558.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--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-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 20261015T151456Z-t1015c-a06-partial.lean, extracted by the gate at 067497e74a8b 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_low hole ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K hole
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K, with h_low : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K.
Left open as a hole; its statement is erdos-1094--h2--h1--h1--h1--h1 (open).
Lean, lines 14–16
```
  have h_low : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k →
      (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-partial.lean, lines 14–16 at 6ba7fea98468 ↗
h_high hole ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K hole
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K, with h_high : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K.
Left open as a hole; its statement is erdos-1094--h2--h1--h1--h1--h2 (open).
Lean, lines 17–19
```
  have h_high : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k →
      (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
    sorry
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-partial.lean, lines 17–19 at 6ba7fea98468 ↗
s3 obtain ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K, with K1 : ℕ, hK1 : ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K1.
Lean, line 20
```
  obtain ⟨K1, hK1⟩ := h_low
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-partial.lean, line 20 at 6ba7fea98468 ↗
s4 obtain ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K, with K2 : ℕ, hK2 : ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K2.
Lean, line 21
```
  obtain ⟨K2, hK2⟩ := h_high
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-partial.lean, line 21 at 6ba7fea98468 ↗
s5 case
Leaves k ≤ max K1 K2, with h : n < k * k.
Uses library le_max_of_le_left.
Lean, line 24
```
  · exact le_max_of_le_left (hK1 n k hk hn h hc hg)
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-partial.lean, line 24 at 6ba7fea98468 ↗
s6 case
Leaves k ≤ max K1 K2, with h : k * k ≤ n.
Uses library le_max_of_le_right.
Lean, line 25
```
  · exact le_max_of_le_right (hK2 n k hk h hn3 hc hg)
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1/attempts/20261015T151456Z-t1015c-a06-partial.lean, line 25 at 6ba7fea98468 ↗

import Mathlib
import Nodes.«erdos-1094--h2--h1--h1--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__h1__h1__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
  -- Split the range 2k ≤ n < k³ at n = k²: the lower band (n < k², Sylvester–Schur/Ecklund
  -- regime) and the upper band (k² ≤ n < k³). Each hole carries a stronger hypothesis.
  have h_low : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k →
      (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
    sorry
  have h_high : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k →
      (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K := by
    sorry
  obtain ⟨K1, hK1⟩ := h_low
  obtain ⟨K2, hK2⟩ := h_high
  refine ⟨max K1 K2, fun n k hk hn hn3 hc hg => ?_⟩
  rcases lt_or_ge n (k * k) with h | h
  · exact le_max_of_le_left (hK1 n k hk hn h hc hg)
  · exact le_max_of_le_right (hK2 n k hk h hn3 hc hg)

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 →