Open Proof Network

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

the thin strip with n/gcd(n,k) prime

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

open

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

$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ 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$ in the strip $k^2\le n<k(k+3k^{21/40})$ (the upper bound taken over the reals, with $21/40$ a real exponent) 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$, and Nat.minFac is the least prime factor (1 at 1, 2 at 0).

unverified · history

Lean
theorem erdos_1094__h2__h1__h4__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          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 these holes by 20261015T145300Z-t1015c-a06-partial.lean (merged in 5ffb3af9f608, attestation 000549).

  • h_cop → erdos-1094--h2--h1--h4--h1--h1 (open)

    $\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ n\text{ prime},\ \ \gcd(n,k)=1\ \Longrightarrow\ k\le K$

  • h_div → erdos-1094--h2--h1--h4--h1--h2 (open)

    $\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ 2\le\gcd(n,k)\ \Longrightarrow\ k\le K$

Read the partial proof (Lean)
theorem erdos_1094__h2__h1__h4__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → k ≤ K := by
  have h_cop : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → n.Prime → n.gcd k = 1 → k ≤ K := by
    sorry
  have h_div : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) →
                2 ≤ n.gcd k → k ≤ K := by
    sorry
  obtain ⟨K1, h1⟩ := h_cop
  obtain ⟨K2, h2⟩ := h_div
  refine ⟨max K1 K2, fun n k hk hn he hd hm hp => ?_⟩
  rcases Nat.lt_or_ge (n.gcd k) 2 with hg | hg
  · have hg1 : n.gcd k = 1 := by
      have := Nat.gcd_pos_of_pos_right n hk
      omega
    have hnp : n.Prime := by
      rw [hg1, Nat.div_one] at hp
      exact hp
    exact le_trans (h1 n k hk hn he hd hm hnp hg1) (le_max_left _ _)
  · exact le_trans (h2 n k hk hn he hd hm hp hg) (le_max_right _ _)

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--h4--h1/attempts/20261015T145300Z-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--h4--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__h4__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → k ≤ K := by
  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 →

In words, unverified — what this statement says; written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-18; no one has read it against the Lean and signed it.

Draft · drafted, by the model named above

$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ 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$ in the strip $k^2\le n<k(k+3k^{21/40})$ (the upper bound taken over the reals, with $21/40$ a real exponent) 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$, and Nat.minFac is the least prime factor (1 at 1, 2 at 0).

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

Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--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--h4--h1--h1: $\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ n\text{ prime},\ \ \gcd(n,k)=1\ \Longrightarrow\ k\le K$
  • erdos-1094--h2--h1--h4--h1--h2: $\exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^2\le n,\ \ n<k\bigl(k+3k^{21/40}\bigr),\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ 2\le\gcd(n,k)\ \Longrightarrow\ k\le K$
Attestation: none of a proof

No proof of this statement has been merged. A partial assembly merged under attestations/000549.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--h4--h1/Witness.lean, sha256 86bdc6976637.
import Mathlib
import Nodes.«erdos-1094--h2--h1--h4--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: route-dead-ends 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 5ffb3af9f608 under attestations/000549.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--h4--h1/attempts/20261015T145300Z-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 20261015T145300Z-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.

  1. h_cop hole ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime n → n.gcd k = (1 : ℕ) → k ≤ K hole

    Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → k ≤ K, with h_cop : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime n → n.gcd k = (1 : ℕ) → k ≤ K.

    Left open as a hole; its statement is erdos-1094--h2--h1--h4--h1--h1 (open).

    Lean, lines 15–21
      have h_cop : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → n.Prime → n.gcd k = 1 → k ≤ K := by
    sorry

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, lines 15–21 at 6ba7fea98468 ↗

  2. h_div hole ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K hole

    Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → k ≤ K, with h_div : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K.

    Uses library Nat.Prime Nat.Prime p means that p is a prime number, that is, a natural number at least 2 whose only divisors are p and 1. .

    Left open as a hole; its statement is erdos-1094--h2--h1--h4--h1--h2 (open).

    Lean, lines 22–29
      have h_div : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) →
                2 ≤ n.gcd k → k ≤ K := by
    sorry

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, lines 22–29 at 6ba7fea98468 ↗

  3. s3 obtain ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime n → n.gcd k = (1 : ℕ) → k ≤ K

    Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → k ≤ K, with K1 : ℕ, h1 : ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime n → n.gcd k = (1 : ℕ) → k ≤ K1.

    Lean, line 30
      obtain ⟨K1, h1⟩ := h_cop

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, line 30 at 6ba7fea98468 ↗

  4. s4 obtain ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K

    Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → k ≤ K, with K2 : ℕ, h2 : ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) → k * (n / k) ∣ k ! → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → (2 : ℕ) ≤ n.gcd k → k ≤ K2.

    Lean, line 31
      obtain ⟨K2, h2⟩ := h_div

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, line 31 at 6ba7fea98468 ↗

  5. s5 case

    Leaves k ≤ max K1 K2, with hg : n.gcd k < (2 : ℕ).

    Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_left.

    Lean, lines 34–40
      · have hg1 : n.gcd k = 1 := by
      have := Nat.gcd_pos_of_pos_right n hk
      omega
    have hnp : n.Prime := by
      rw [hg1, Nat.div_one] at hp
      exact hp
    exact le_trans (h1 n k hk hn he hd hm hnp hg1) (le_max_left _ _)

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, lines 34–40 at 6ba7fea98468 ↗

    1. s5.hg1 have n.gcd k = (1 : ℕ)

      Leaves k ≤ max K1 K2, with hg1 : n.gcd k = (1 : ℕ).

      Lean, lines 34–36
        · have hg1 : n.gcd k = 1 := by
      have := Nat.gcd_pos_of_pos_right n hk
      omega

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, lines 34–36 at 6ba7fea98468 ↗

      1. s5.hg1.this have (0 : ℕ) < n.gcd k

        Leaves n.gcd k = (1 : ℕ), with this : (0 : ℕ) < n.gcd k.

        Uses library Nat.gcd_pos_of_pos_right.

        Lean, line 35
              have := Nat.gcd_pos_of_pos_right n hk

        targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, line 35 at 6ba7fea98468 ↗

    2. s5.hnp have Nat.Prime n

      Leaves k ≤ max K1 K2, with hnp : Nat.Prime n.

      Uses library Nat.div_one.

      Lean, lines 37–39
          have hnp : n.Prime := by
      rw [hg1, Nat.div_one] at hp
      exact hp

      targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, lines 37–39 at 6ba7fea98468 ↗

  6. s6 case

    Leaves k ≤ max K1 K2, with hg : n.gcd k ≥ (2 : ℕ).

    Uses library le_trans The relation ≤ on a preorder is transitive. , le_max_right.

    Lean, line 41
      · exact le_trans (h2 n k hk hn he hd hm hp hg) (le_max_right _ _)

    targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1/attempts/20261015T145300Z-t1015c-a06-partial.lean, line 41 at 6ba7fea98468 ↗

import Mathlib
import Nodes.«erdos-1094--h2--h1--h4--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__h4__h1 : ∃ (K : ℕ),
  ∀ (n k : ℕ),
    (0 : ℕ) < k →
      k * k ≤ n →
        (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
          k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → k ≤ K := by
  have h_cop : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → n.Prime → n.gcd k = 1 → k ≤ K := by
    sorry
  have h_div : ∃ (K : ℕ),
      ∀ (n k : ℕ),
        (0 : ℕ) < k →
          k * k ≤ n →
            (↑n : ℝ) < (↑k : ℝ) * ((↑k : ℝ) + (3 : ℝ) * (↑k : ℝ) ^ (21 / 40 : ℝ)) →
              k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) →
                2 ≤ n.gcd k → k ≤ K := by
    sorry
  obtain ⟨K1, h1⟩ := h_cop
  obtain ⟨K2, h2⟩ := h_div
  refine ⟨max K1 K2, fun n k hk hn he hd hm hp => ?_⟩
  rcases Nat.lt_or_ge (n.gcd k) 2 with hg | hg
  · have hg1 : n.gcd k = 1 := by
      have := Nat.gcd_pos_of_pos_right n hk
      omega
    have hnp : n.Prime := by
      rw [hg1, Nat.div_one] at hp
      exact hp
    exact le_trans (h1 n k hk hn he hd hm hnp hg1) (le_max_left _ _)
  · exact le_trans (h2 n k hk hn he hd hm hp hg) (le_max_right _ _)
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 →