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

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

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

open

Hole h_low of erdos-1094--h2--h1--h1--h1 (split by 20261015T151456Z-t1015c-a06-partial.lean).

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

Only finitely many $k$ admit an $n$ with $2k\le n<k^2$ 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^2$ as 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__h1 : ∃ (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

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 20261018T192600Z-t1018-a-partial.lean (merged in e493ea815aa2, attestation 000760).

h_prime → erdos-1094--h2--h1--h1--h1--h1--h1 (open)
$\displaystyle \exists K\ \forall n,k:\ 2k\le n<k^2,\ n \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
h_comp → erdos-1094--h2--h1--h1--h1--h1--h2 (open)
$\displaystyle \exists K\ \forall n,k,q:\ 2k\le n<k^2,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \gcd(n,k)\ge2,\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$

Read the partial proof (Lean)

theorem erdos_1094__h2__h1__h1__h1__h1 : ∃ (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
  -- approach: m = n/gcd(n,k) has minFac > k and m < k^2, so m is a prime q > k; split n = q (n prime) from n = g*q with 2 <= g | k
  -- licence: CC-BY-4.0
  have hall : (∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
        (n.choose k).minFac > k → n.Prime → k ≤ K) ∧
      (∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
        (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K) := by
    refine ⟨?_, ?_⟩
    ·
      -- label: n prime in [2k, k^2)
      -- claim: $\exists K\ \forall n,k:\ 2k\le n<k^2,\ n \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_prime : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
          (n.choose k).minFac > k → n.Prime → k ≤ K := by
        sorry
      exact h_prime
    ·
      -- label: n = g q with 2 <= g | k and q > k prime
      -- claim: $\exists K\ \forall n,k,q:\ 2k\le n<k^2,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \gcd(n,k)\ge2,\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_comp : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
          (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K := by
        sorry
      exact h_comp
  obtain ⟨⟨K1, hK1⟩, ⟨K2, hK2⟩⟩ := hall
  refine ⟨max K1 K2, fun n k hk hn hnk hc hg => ?_⟩
  have hgpos : 0 < n.gcd k := Nat.gcd_pos_of_pos_right n hk
  have hgk : n.gcd k ≤ k := Nat.le_of_dvd hk (Nat.gcd_dvd_right n k)
  have hnm : n = n.gcd k * (n / n.gcd k) := (Nat.mul_div_cancel' (Nat.gcd_dvd_left n k)).symm
  have hmn : n / n.gcd k ≤ n := Nat.div_le_self n _
  have hm2 : 2 ≤ n / n.gcd k := by
    by_contra h
    have h' : n / n.gcd k ≤ 1 := by omega
    have : n ≤ n.gcd k := by
      calc n = n.gcd k * (n / n.gcd k) := hnm
        _ ≤ n.gcd k * 1 := Nat.mul_le_mul_left _ h'
        _ = n.gcd k := Nat.mul_one _
    omega
  have hmprime : (n / n.gcd k).Prime := by
    by_contra hnp
    have h1 := Nat.minFac_sq_le_self (by omega : 0 < n / n.gcd k) hnp
    have h2 : k * k < (n / n.gcd k).minFac ^ 2 := by
      rw [pow_two]; exact Nat.mul_lt_mul'' hg hg
    omega
  have hkm : k < n / n.gcd k := lt_of_lt_of_le hg (Nat.minFac_le (by omega))
  by_cases hg1 : n.gcd k = 1
  · have hn' : n = n / n.gcd k := by
      conv_lhs => rw [hnm, hg1, one_mul]
      rw [hg1]
    have hnp : n.Prime := by rw [hn']; exact hmprime
    exact le_max_of_le_left (hK1 n k hk hn hnk hc hnp)
  · exact le_max_of_le_right (hK2 n k (n / n.gcd k) hk hn hnk hc hmprime hkm (by omega) hnm)

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--h1/attempts/20261018T192600Z-t1018-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

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--h1».Context

open scoped Nat

/-! Hole `h_low` 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__h1 : ∃ (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

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/6289e73b1bc6….md · Improve these words →

Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--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--h1: $\exists K\ \forall n,k:\ 2k\le n<k^2,\ n \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
erdos-1094--h2--h1--h1--h1--h1--h2: $\exists K\ \forall n,k,q:\ 2k\le n<k^2,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \gcd(n,k)\ge2,\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$

Attestation: none of a proof

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

import Mathlib
import Nodes.«erdos-1094--h2--h1--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: budget-exhausted 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 t1018-a; merged in e493ea815aa2 under attestations/000760.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--h1/attempts/20261018T192600Z-t1018-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 20261018T192600Z-t1018-a-partial.lean, extracted by the gate at 32961c7678e9 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.

hall have (∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime n → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (n / n.gcd k).minFac > k → k ≤ K, with hall : (∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime n → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K.
Uses library And.intro.
Lean, lines 13–31
```
  have hall : (∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
        (n.choose k).minFac > k → n.Prime → k ≤ K) ∧
      (∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
        (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K) := by
    refine ⟨?_, ?_⟩
    ·
      -- label: n prime in [2k, k^2)
      -- claim: $\exists K\ \forall n,k:\ 2k\le n<k^2,\ n \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_prime : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
          (n.choose k).minFac > k → n.Prime → k ≤ K := by
        sorry
      exact h_prime
    ·
      -- label: n = g q with 2 <= g | k and q > k prime
      -- claim: $\exists K\ \forall n,k,q:\ 2k\le n<k^2,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \gcd(n,k)\ge2,\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_comp : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
          (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K := by
        sorry
      exact h_comp
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 13–31 at f0dfc93f9827 ↗
1. hall.s1 case
  Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime n → k ≤ K.
  Lean, lines 18–24
  · -- label: n prime in [2k, k^2) -- claim: $\exists K\ \forall n,k:\ 2k\le n<k^2,\ n \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$ have h_prime : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k → (n.choose k).minFac > k → n.Prime → k ≤ K := by sorry exact h_prime
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 18–24 at f0dfc93f9827 ↗
  hall.s1.h_prime hole ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime n → k ≤ K hole
  Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime n → k ≤ K, with h_prime : ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime n → k ≤ K.
  Left open as a hole; its statement is erdos-1094--h2--h1--h1--h1--h1--h1 (open).
  Lean, lines 21–23
  have h_prime : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k → (n.choose k).minFac > k → n.Prime → k ≤ K := by sorry
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 21–23 at f0dfc93f9827 ↗
2. hall.s2 case
  Leaves ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K.
  Lean, lines 25–31
  · -- label: n = g q with 2 <= g | k and q > k prime -- claim: $\exists K\ \forall n,k,q:\ 2k\le n<k^2,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \gcd(n,k)\ge2,\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$ have h_comp : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k → (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K := by sorry exact h_comp
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 25–31 at f0dfc93f9827 ↗
  hall.s2.h_comp hole ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K hole
  Leaves ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K, with h_comp : ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K.
  Left open as a hole; its statement is erdos-1094--h2--h1--h1--h1--h1--h2 (open).
  Lean, lines 28–30
  have h_comp : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k → (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K := by sorry
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 28–30 at f0dfc93f9827 ↗
s2 obtain (∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime n → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K
Leaves ∃ (K : ℕ), ∀ (n k : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < 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 → Nat.Prime n → k ≤ K1, K2 : ℕ, hK2 : ∀ (n k q : ℕ), (0 : ℕ) < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → (2 : ℕ) ≤ n.gcd k → n = n.gcd k * q → k ≤ K2.
Lean, line 32
```
  obtain ⟨⟨K1, hK1⟩, ⟨K2, hK2⟩⟩ := hall
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 32 at f0dfc93f9827 ↗
hgpos have (0 : ℕ) < n.gcd k
Leaves k ≤ max K1 K2, with hgpos : (0 : ℕ) < n.gcd k.
Uses library Nat.gcd_pos_of_pos_right.
Lean, line 34
```
  have hgpos : 0 < n.gcd k := Nat.gcd_pos_of_pos_right n hk
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 34 at f0dfc93f9827 ↗
hgk have n.gcd k ≤ k
Leaves k ≤ max K1 K2, with hgk : n.gcd k ≤ k.
Uses library Nat.le_of_dvd, Nat.gcd_dvd_right.
Lean, line 35
```
  have hgk : n.gcd k ≤ k := Nat.le_of_dvd hk (Nat.gcd_dvd_right n k)
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 35 at f0dfc93f9827 ↗
hnm have n = n.gcd k * (n / n.gcd k)
Leaves k ≤ max K1 K2, with hnm : n = n.gcd k * (n / n.gcd k).
Uses library Nat.mul_div_cancel', Nat.gcd_dvd_left.
Lean, line 36
```
  have hnm : n = n.gcd k * (n / n.gcd k) := (Nat.mul_div_cancel' (Nat.gcd_dvd_left n k)).symm
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 36 at f0dfc93f9827 ↗
hmn have n / n.gcd k ≤ n
Leaves k ≤ max K1 K2, with hmn : n / n.gcd k ≤ n.
Uses library Nat.div_le_self.
Lean, line 37
```
  have hmn : n / n.gcd k ≤ n := Nat.div_le_self n _
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 37 at f0dfc93f9827 ↗
hm2 have (2 : ℕ) ≤ n / n.gcd k
Leaves k ≤ max K1 K2, with hm2 : (2 : ℕ) ≤ n / n.gcd k.
Lean, lines 38–45
```
  have hm2 : 2 ≤ n / n.gcd k := by
    by_contra h
    have h' : n / n.gcd k ≤ 1 := by omega
    have : n ≤ n.gcd k := by
      calc n = n.gcd k * (n / n.gcd k) := hnm
        _ ≤ n.gcd k * 1 := Nat.mul_le_mul_left _ h'
        _ = n.gcd k := Nat.mul_one _
    omega
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 38–45 at f0dfc93f9827 ↗
1. hm2.h' have n / n.gcd k ≤ (1 : ℕ) routine: omega
  Leaves False, with h' : n / n.gcd k ≤ (1 : ℕ).
  Lean, line 40
  have h' : n / n.gcd k ≤ 1 := by omega
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 40 at f0dfc93f9827 ↗
2. hm2.this have n ≤ n.gcd k
  Leaves False, with this : n ≤ n.gcd k.
  Lean, lines 41–44
  have : n ≤ n.gcd k := by calc n = n.gcd k * (n / n.gcd k) := hnm _ ≤ n.gcd k * 1 := Nat.mul_le_mul_left _ h' _ = n.gcd k := Nat.mul_one _
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 41–44 at f0dfc93f9827 ↗
  hm2.this.s1 calc n = n.gcd k * (n / n.gcd k)
  Closes the goal.
  Lean, line 42
  calc n = n.gcd k * (n / n.gcd k) := hnm
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 42 at f0dfc93f9827 ↗
  hm2.this.s2 calc n.gcd k * (n / n.gcd k) ≤ n.gcd k * (1 : ℕ)
  Closes the goal.
  Uses library Nat.mul_le_mul_left.
  Lean, line 43
  _ ≤ n.gcd k * 1 := Nat.mul_le_mul_left _ h'
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 43 at f0dfc93f9827 ↗
  hm2.this.s3 calc n.gcd k * (1 : ℕ) = n.gcd k
  Closes the goal.
  Uses library Nat.mul_one.
  Lean, line 44
  _ = n.gcd k := Nat.mul_one _
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 44 at f0dfc93f9827 ↗
hmprime have Nat.Prime (n / n.gcd k)
Leaves k ≤ max K1 K2, with hmprime : Nat.Prime (n / n.gcd k).
Lean, lines 46–51
```
  have hmprime : (n / n.gcd k).Prime := by
    by_contra hnp
    have h1 := Nat.minFac_sq_le_self (by omega : 0 < n / n.gcd k) hnp
    have h2 : k * k < (n / n.gcd k).minFac ^ 2 := by
      rw [pow_two]; exact Nat.mul_lt_mul'' hg hg
    omega
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 46–51 at f0dfc93f9827 ↗
1. hmprime.h1 have (n / n.gcd k).minFac ^ (2 : ℕ) ≤ n / n.gcd k
  Leaves False, with h1 : (n / n.gcd k).minFac ^ (2 : ℕ) ≤ n / n.gcd k.
  Uses library Nat.minFac_sq_le_self.
  Lean, line 48
  have h1 := Nat.minFac_sq_le_self (by omega : 0 < n / n.gcd k) hnp
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 48 at f0dfc93f9827 ↗
2. hmprime.h2 have k * k < (n / n.gcd k).minFac ^ (2 : ℕ)
  Leaves False, with h2 : k * k < (n / n.gcd k).minFac ^ (2 : ℕ).
  Uses library pow_two, Nat.mul_lt_mul''.
  Lean, lines 49–50
  have h2 : k * k < (n / n.gcd k).minFac ^ 2 := by rw [pow_two]; exact Nat.mul_lt_mul'' hg hg
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 49–50 at f0dfc93f9827 ↗
hkm have k < n / n.gcd k
Leaves k ≤ max K1 K2, with hkm : k < n / n.gcd k.
Uses library lt_of_lt_of_le, Nat.minFac_le.
Lean, line 52
```
  have hkm : k < n / n.gcd k := lt_of_lt_of_le hg (Nat.minFac_le (by omega))
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 52 at f0dfc93f9827 ↗
s10 case
Leaves k ≤ max K1 K2, with hg1 : n.gcd k = (1 : ℕ).
Uses library le_max_of_le_left.
Lean, lines 54–58
```
  · have hn' : n = n / n.gcd k := by
      conv_lhs => rw [hnm, hg1, one_mul]
      rw [hg1]
    have hnp : n.Prime := by rw [hn']; exact hmprime
    exact le_max_of_le_left (hK1 n k hk hn hnk hc hnp)
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 54–58 at f0dfc93f9827 ↗
1. s10.hn' have n = n / n.gcd k
  Leaves k ≤ max K1 K2, with hn' : n = n / n.gcd k.
  Uses library one_mul.
  Lean, lines 54–56
  · have hn' : n = n / n.gcd k := by conv_lhs => rw [hnm, hg1, one_mul] rw [hg1]
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, lines 54–56 at f0dfc93f9827 ↗
2. s10.hnp have Nat.Prime n
  Leaves k ≤ max K1 K2, with hnp : Nat.Prime n.
  Lean, line 57
  have hnp : n.Prime := by rw [hn']; exact hmprime
  targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 57 at f0dfc93f9827 ↗
s11 case
Leaves k ≤ max K1 K2, with hg1 : ¬n.gcd k = (1 : ℕ).
Uses library le_max_of_le_right.
Lean, line 59
```
  · exact le_max_of_le_right (hK2 n k (n / n.gcd k) hk hn hnk hc hmprime hkm (by omega) hnm)
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h1/attempts/20261018T192600Z-t1018-a-partial.lean, line 59 at f0dfc93f9827 ↗

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

open scoped Nat

/-! Hole `h_low` 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__h1 : ∃ (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
  -- approach: m = n/gcd(n,k) has minFac > k and m < k^2, so m is a prime q > k; split n = q (n prime) from n = g*q with 2 <= g | k
  -- licence: CC-BY-4.0
  have hall : (∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
        (n.choose k).minFac > k → n.Prime → k ≤ K) ∧
      (∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
        (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K) := by
    refine ⟨?_, ?_⟩
    ·
      -- label: n prime in [2k, k^2)
      -- claim: $\exists K\ \forall n,k:\ 2k\le n<k^2,\ n \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_prime : ∃ K : ℕ, ∀ n k : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
          (n.choose k).minFac > k → n.Prime → k ≤ K := by
        sorry
      exact h_prime
    ·
      -- label: n = g q with 2 <= g | k and q > k prime
      -- claim: $\exists K\ \forall n,k,q:\ 2k\le n<k^2,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \gcd(n,k)\ge2,\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_comp : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → 2 * k ≤ n → n < k * k →
          (n.choose k).minFac > k → q.Prime → k < q → 2 ≤ n.gcd k → n = n.gcd k * q → k ≤ K := by
        sorry
      exact h_comp
  obtain ⟨⟨K1, hK1⟩, ⟨K2, hK2⟩⟩ := hall
  refine ⟨max K1 K2, fun n k hk hn hnk hc hg => ?_⟩
  have hgpos : 0 < n.gcd k := Nat.gcd_pos_of_pos_right n hk
  have hgk : n.gcd k ≤ k := Nat.le_of_dvd hk (Nat.gcd_dvd_right n k)
  have hnm : n = n.gcd k * (n / n.gcd k) := (Nat.mul_div_cancel' (Nat.gcd_dvd_left n k)).symm
  have hmn : n / n.gcd k ≤ n := Nat.div_le_self n _
  have hm2 : 2 ≤ n / n.gcd k := by
    by_contra h
    have h' : n / n.gcd k ≤ 1 := by omega
    have : n ≤ n.gcd k := by
      calc n = n.gcd k * (n / n.gcd k) := hnm
        _ ≤ n.gcd k * 1 := Nat.mul_le_mul_left _ h'
        _ = n.gcd k := Nat.mul_one _
    omega
  have hmprime : (n / n.gcd k).Prime := by
    by_contra hnp
    have h1 := Nat.minFac_sq_le_self (by omega : 0 < n / n.gcd k) hnp
    have h2 : k * k < (n / n.gcd k).minFac ^ 2 := by
      rw [pow_two]; exact Nat.mul_lt_mul'' hg hg
    omega
  have hkm : k < n / n.gcd k := lt_of_lt_of_le hg (Nat.minFac_le (by omega))
  by_cases hg1 : n.gcd k = 1
  · have hn' : n = n / n.gcd k := by
      conv_lhs => rw [hnm, hg1, one_mul]
      rw [hg1]
    have hnp : n.Prime := by rw [hn']; exact hmprime
    exact le_max_of_le_left (hK1 n k hk hn hnk hc hnp)
  · exact le_max_of_le_right (hK2 n k (n / n.gcd k) hk hn hnk hc hmprime hkm (by omega) hnm)

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 →