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

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

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

open

Hole h_high 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,\ \ 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$

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

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 20261018T193800Z-t1018-a-partial.lean (merged in 61359fba2743, attestation 000763).

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

Read the partial proof (Lean)

theorem erdos_1094__h2__h1__h1__h1__h2 : ∃ (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
  -- approach: m = n/gcd(n,k) has every prime factor > k and m < k^3, so m is a prime q or a product p*q of two primes > k
  -- licence: CC-BY-4.0
  have hall : (∃ K : ℕ, ∀ n k q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → q.Prime → k < q → n = n.gcd k * q → k ≤ K) ∧
      (∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → p.Prime → q.Prime → k < p → k < q →
          n = n.gcd k * (p * q) → k ≤ K) := by
    refine ⟨?_, ?_⟩
    ·
      -- label: n = gcd(n,k) times one prime q > k
      -- claim: $\exists K\ \forall n,k,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_one : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → q.Prime → k < q → n = n.gcd k * q → k ≤ K := by
        sorry
      exact h_one
    ·
      -- label: n = gcd(n,k) times p q, two primes > k
      -- claim: $\exists K\ \forall n,k,p,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,pq,\ p,q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_two : ∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → p.Prime → q.Prime → k < p → k < q →
          n = n.gcd k * (p * q) → k ≤ K := by
        sorry
      exact h_two
  obtain ⟨⟨K1, hK1⟩, ⟨K2, hK2⟩⟩ := hall
  refine ⟨max K1 K2, fun n k hk hn hn3 hc hg => ?_⟩
  have hkk : 0 < k * k := Nat.mul_pos hk hk
  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 hm1 : n / n.gcd k ≠ 1 := by
    intro h
    rw [h, Nat.minFac_one] at hg
    omega
  have hm0 : n / n.gcd k ≠ 0 := by
    intro h
    rw [h, Nat.mul_zero] at hnm
    omega
  by_cases hp : (n / n.gcd k).Prime
  · exact le_max_of_le_left
      (hK1 n k _ hk hn hn3 hc hp (lt_of_lt_of_le hg (Nat.minFac_le (Nat.pos_of_ne_zero hm0))) hnm)
  · have hpp : (n / n.gcd k).minFac.Prime := Nat.minFac_prime hm1
    obtain ⟨r, hr⟩ := Nat.minFac_dvd (n / n.gcd k)
    have hr1 : r ≠ 1 := by
      intro h
      rw [h, Nat.mul_one] at hr
      exact hp (hr ▸ hpp)
    have hr0 : r ≠ 0 := by
      intro h
      rw [h, Nat.mul_zero] at hr
      exact hm0 hr
    have hrf : r.minFac > k := by
      have : (n / n.gcd k).minFac ≤ r.minFac :=
        Nat.minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
          (by rw [hr]; exact Dvd.dvd.mul_left (Nat.minFac_dvd r) _)
      omega
    have hrp : r.Prime := by
      by_contra hnr
      have h1 := Nat.minFac_sq_le_self (by omega : 0 < r) hnr
      have h2 : k * k < r.minFac ^ 2 := by
        rw [pow_two]; exact Nat.mul_lt_mul'' hrf hrf
      have h3 : k * (k * k) < (n / n.gcd k).minFac * r := Nat.mul_lt_mul'' hg (by omega)
      have e : k * k * k = k * (k * k) := Nat.mul_assoc _ _ _
      omega
    exact le_max_of_le_right (hK2 n k _ r hk hn hn3 hc hpp hrp hg
      (lt_of_lt_of_le hrf (Nat.minFac_le (by omega))) (by rw [← hr]; exact 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--h2/attempts/20261018T193800Z-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--h2».Context

open scoped Nat

/-! Hole `h_high` 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__h2 : ∃ (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

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

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

import Mathlib
import Nodes.«erdos-1094--h2--h1--h1--h1--h2».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 61359fba2743 under attestations/000763.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--h2/attempts/20261018T193800Z-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 20261018T193800Z-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 q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k p q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime p → Nat.Prime q → k k → (n / n.gcd k).minFac > k → k ≤ K, with hall : (∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k p q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime p → Nat.Prime q → k k → q.Prime → k < q → n = n.gcd k * q → k ≤ K) ∧
 (∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
 (n.choose k).minFac > k → p.Prime → q.Prime → k k
 -- claim: $\exists K\ \forall n,k,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
 have h_one : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
 (n.choose k).minFac > k → q.Prime → k < q → n = n.gcd k * q → k ≤ K := by
 sorry
 exact h_one
 ·
 -- label: n = gcd(n,k) times p q, two primes > k
 -- claim: $\exists K\ \forall n,k,p,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,pq,\ p,q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
 have h_two : ∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
 (n.choose k).minFac > k → p.Prime → q.Prime → k < p → k < q →
 n = n.gcd k * (p * q) → k ≤ K := by
 sorry
 exact h_two
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 13–33 at f0dfc93f9827 ↗
1. hall.s1 case
 Leaves ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K.
 Lean, lines 19–25
 · -- label: n = gcd(n,k) times one prime q > k -- claim: $\exists K\ \forall n,k,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$ have h_one : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → q.Prime → k < q → n = n.gcd k * q → k ≤ K := by sorry exact h_one
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 19–25 at f0dfc93f9827 ↗
 hall.s1.h_one hole ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K hole
 Leaves ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K, with h_one : ∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K.
 Left open as a hole; its statement is erdos-1094--h2--h1--h1--h1--h2--h1 (open).
 Lean, lines 22–24
 have h_one : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → q.Prime → k < q → n = n.gcd k * q → k ≤ K := by sorry
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 22–24 at f0dfc93f9827 ↗
2. hall.s2 case
 Leaves ∃ (K : ℕ), ∀ (n k p q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime p → Nat.Prime q → k k -- claim: $\exists K\ \forall n,k,p,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,pq,\ p,q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$ have h_two : ∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → p.Prime → q.Prime → k < p → k < q → n = n.gcd k * (p * q) → k ≤ K := by sorry exact h_two
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 26–33 at f0dfc93f9827 ↗
 hall.s2.h_two hole ∃ (K : ℕ), ∀ (n k p q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime p → Nat.Prime q → k k → Nat.Prime p → Nat.Prime q → k k → Nat.Prime p → Nat.Prime q → k < p → k < q → n = n.gcd k * (p * q) → k ≤ K.
 Left open as a hole; its statement is erdos-1094--h2--h1--h1--h1--h2--h2 (open).
 Lean, lines 29–32
 have h_two : ∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → p.Prime → q.Prime → k < p → k < q → n = n.gcd k * (p * q) → k ≤ K := by sorry
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 29–32 at f0dfc93f9827 ↗
s2 obtain (∃ (K : ℕ), ∀ (n k q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K) ∧ ∃ (K : ℕ), ∀ (n k p q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime p → Nat.Prime q → k k → (n / n.gcd k).minFac > k → k ≤ K, with K1 : ℕ, hK1 : ∀ (n k q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime q → k < q → n = n.gcd k * q → k ≤ K1, K2 : ℕ, hK2 : ∀ (n k p q : ℕ), (0 : ℕ) < k → k * k ≤ n → n < k * k * k → (n.choose k).minFac > k → Nat.Prime p → Nat.Prime q → k < p → k < q → n = n.gcd k * (p * q) → k ≤ K2.
Lean, line 34
```
 obtain ⟨⟨K1, hK1⟩, ⟨K2, hK2⟩⟩ := hall
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 34 at f0dfc93f9827 ↗
hkk have (0 : ℕ) < k * k
Leaves k ≤ max K1 K2, with hkk : (0 : ℕ) < k * k.
Uses library Nat.mul_pos.
Lean, line 36
```
 have hkk : 0 < k * k := Nat.mul_pos hk hk
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 36 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 37
```
  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--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 37 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 38
```
  have hmn : n / n.gcd k ≤ n := Nat.div_le_self n _
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 38 at f0dfc93f9827 ↗
hm1 have n / n.gcd k ≠ (1 : ℕ)
Leaves k ≤ max K1 K2, with hm1 : n / n.gcd k ≠ (1 : ℕ).
Uses library Nat.minFac_one.
Lean, lines 39–42
```
  have hm1 : n / n.gcd k ≠ 1 := by
    intro h
    rw [h, Nat.minFac_one] at hg
    omega
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 39–42 at f0dfc93f9827 ↗
hm0 have n / n.gcd k ≠ (0 : ℕ)
Leaves k ≤ max K1 K2, with hm0 : n / n.gcd k ≠ (0 : ℕ).
Uses library Nat.mul_zero.
Lean, lines 43–46
```
  have hm0 : n / n.gcd k ≠ 0 := by
    intro h
    rw [h, Nat.mul_zero] at hnm
    omega
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 43–46 at f0dfc93f9827 ↗
s8 case
Leaves k ≤ max K1 K2, with hp : Nat.Prime (n / n.gcd k).
Uses library le_max_of_le_left, lt_of_lt_of_le, Nat.minFac_le, Nat.pos_of_ne_zero.
Lean, lines 48–49
```
  · exact le_max_of_le_left
      (hK1 n k _ hk hn hn3 hc hp (lt_of_lt_of_le hg (Nat.minFac_le (Nat.pos_of_ne_zero hm0))) hnm)
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 48–49 at f0dfc93f9827 ↗
s9 case
Leaves k ≤ max K1 K2, with hp : ¬Nat.Prime (n / n.gcd k).
Uses library le_max_of_le_right, lt_of_lt_of_le, Nat.minFac_le.
Lean, lines 50–74
```
 · have hpp : (n / n.gcd k).minFac.Prime := Nat.minFac_prime hm1
 obtain ⟨r, hr⟩ := Nat.minFac_dvd (n / n.gcd k)
 have hr1 : r ≠ 1 := by
 intro h
 rw [h, Nat.mul_one] at hr
 exact hp (hr ▸ hpp)
 have hr0 : r ≠ 0 := by
 intro h
 rw [h, Nat.mul_zero] at hr
 exact hm0 hr
 have hrf : r.minFac > k := by
 have : (n / n.gcd k).minFac ≤ r.minFac :=
 Nat.minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
 (by rw [hr]; exact Dvd.dvd.mul_left (Nat.minFac_dvd r) _)
 omega
 have hrp : r.Prime := by
 by_contra hnr
 have h1 := Nat.minFac_sq_le_self (by omega : 0 < r) hnr
 have h2 : k * k < r.minFac ^ 2 := by
 rw [pow_two]; exact Nat.mul_lt_mul'' hrf hrf
 have h3 : k * (k * k) < (n / n.gcd k).minFac * r := Nat.mul_lt_mul'' hg (by omega)
 have e : k * k * k = k * (k * k) := Nat.mul_assoc _ _ _
 omega
 exact le_max_of_le_right (hK2 n k _ r hk hn hn3 hc hpp hrp hg
 (lt_of_lt_of_le hrf (Nat.minFac_le (by omega))) (by rw [← hr]; exact hnm))
```
targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 50–74 at f0dfc93f9827 ↗
1. s9.hpp have Nat.Prime (n / n.gcd k).minFac
 Leaves k ≤ max K1 K2, with hpp : Nat.Prime (n / n.gcd k).minFac.
 Uses library Nat.minFac_prime.
 Lean, line 50
 · have hpp : (n / n.gcd k).minFac.Prime := Nat.minFac_prime hm1
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 50 at f0dfc93f9827 ↗
2. s9.s2 obtain (n / n.gcd k).minFac ∣ n / n.gcd k
 Leaves k ≤ max K1 K2, with r : ℕ, hr : n / n.gcd k = (n / n.gcd k).minFac * r.
 Uses library Nat.minFac_dvd.
 Lean, line 51
 obtain ⟨r, hr⟩ := Nat.minFac_dvd (n / n.gcd k)
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 51 at f0dfc93f9827 ↗
3. s9.hr1 have r ≠ (1 : ℕ)
 Leaves k ≤ max K1 K2, with hr1 : r ≠ (1 : ℕ).
 Uses library Nat.mul_one.
 Lean, lines 52–55
 have hr1 : r ≠ 1 := by intro h rw [h, Nat.mul_one] at hr exact hp (hr ▸ hpp)
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 52–55 at f0dfc93f9827 ↗
4. s9.hr0 have r ≠ (0 : ℕ)
 Leaves k ≤ max K1 K2, with hr0 : r ≠ (0 : ℕ).
 Uses library Nat.mul_zero.
 Lean, lines 56–59
 have hr0 : r ≠ 0 := by intro h rw [h, Nat.mul_zero] at hr exact hm0 hr
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 56–59 at f0dfc93f9827 ↗
5. s9.hrf have r.minFac > k
 Leaves k ≤ max K1 K2, with hrf : r.minFac > k.
 Lean, lines 60–64
 have hrf : r.minFac > k := by have : (n / n.gcd k).minFac ≤ r.minFac := Nat.minFac_le_of_dvd (Nat.minFac_prime hr1).two_le (by rw [hr]; exact Dvd.dvd.mul_left (Nat.minFac_dvd r) _) omega
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 60–64 at f0dfc93f9827 ↗
 s9.hrf.this have (n / n.gcd k).minFac ≤ r.minFac
 Leaves r.minFac > k, with this : (n / n.gcd k).minFac ≤ r.minFac.
 Uses library Nat.minFac_le_of_dvd, Nat.minFac_prime, Dvd.dvd.mul_left, Nat.minFac_dvd.
 Lean, lines 61–63
 have : (n / n.gcd k).minFac ≤ r.minFac := Nat.minFac_le_of_dvd (Nat.minFac_prime hr1).two_le (by rw [hr]; exact Dvd.dvd.mul_left (Nat.minFac_dvd r) _)
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 61–63 at f0dfc93f9827 ↗
6. s9.hrp have Nat.Prime r
 Leaves k ≤ max K1 K2, with hrp : Nat.Prime r.
 Lean, lines 65–72
 have hrp : r.Prime := by by_contra hnr have h1 := Nat.minFac_sq_le_self (by omega : 0 < r) hnr have h2 : k * k < r.minFac ^ 2 := by rw [pow_two]; exact Nat.mul_lt_mul'' hrf hrf have h3 : k * (k * k) < (n / n.gcd k).minFac * r := Nat.mul_lt_mul'' hg (by omega) have e : k * k * k = k * (k * k) := Nat.mul_assoc _ _ _ omega
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 65–72 at f0dfc93f9827 ↗
 s9.hrp.h1 have r.minFac ^ (2 : ℕ) ≤ r
 Leaves False, with h1 : r.minFac ^ (2 : ℕ) ≤ r.
 Uses library Nat.minFac_sq_le_self.
 Lean, line 67
 have h1 := Nat.minFac_sq_le_self (by omega : 0 < r) hnr
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 67 at f0dfc93f9827 ↗
 s9.hrp.h2 have k * k < r.minFac ^ (2 : ℕ)
 Leaves False, with h2 : k * k < r.minFac ^ (2 : ℕ).
 Uses library pow_two, Nat.mul_lt_mul''.
 Lean, lines 68–69
 have h2 : k * k < r.minFac ^ 2 := by rw [pow_two]; exact Nat.mul_lt_mul'' hrf hrf
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, lines 68–69 at f0dfc93f9827 ↗
 s9.hrp.h3 have k * (k * k) < (n / n.gcd k).minFac * r
 Leaves False, with h3 : k * (k * k) < (n / n.gcd k).minFac * r.
 Uses library Nat.mul_lt_mul''.
 Lean, line 70
 have h3 : k * (k * k) < (n / n.gcd k).minFac * r := Nat.mul_lt_mul'' hg (by omega)
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 70 at f0dfc93f9827 ↗
 s9.hrp.e have k * k * k = k * (k * k)
 Leaves False, with e : k * k * k = k * (k * k).
 Uses library Nat.mul_assoc.
 Lean, line 71
 have e : k * k * k = k * (k * k) := Nat.mul_assoc _ _ _
 targets/erdos-1094/nodes/erdos-1094--h2--h1--h1--h1--h2/attempts/20261018T193800Z-t1018-a-partial.lean, line 71 at f0dfc93f9827 ↗

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

open scoped Nat

/-! Hole `h_high` 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__h2 : ∃ (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
  -- approach: m = n/gcd(n,k) has every prime factor > k and m < k^3, so m is a prime q or a product p*q of two primes > k
  -- licence: CC-BY-4.0
  have hall : (∃ K : ℕ, ∀ n k q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → q.Prime → k < q → n = n.gcd k * q → k ≤ K) ∧
      (∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → p.Prime → q.Prime → k < p → k < q →
          n = n.gcd k * (p * q) → k ≤ K) := by
    refine ⟨?_, ?_⟩
    ·
      -- label: n = gcd(n,k) times one prime q > k
      -- claim: $\exists K\ \forall n,k,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,q,\ q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_one : ∃ K : ℕ, ∀ n k q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → q.Prime → k < q → n = n.gcd k * q → k ≤ K := by
        sorry
      exact h_one
    ·
      -- label: n = gcd(n,k) times p q, two primes > k
      -- claim: $\exists K\ \forall n,k,p,q:\ k^2\le n<k^3,\ n=\gcd(n,k)\,pq,\ p,q>k \text{ prime},\ \operatorname{minFac}\binom nk>k \Rightarrow k\le K$
      have h_two : ∃ K : ℕ, ∀ n k p q : ℕ, 0 < k → k * k ≤ n → n < k * k * k →
          (n.choose k).minFac > k → p.Prime → q.Prime → k < p → k < q →
          n = n.gcd k * (p * q) → k ≤ K := by
        sorry
      exact h_two
  obtain ⟨⟨K1, hK1⟩, ⟨K2, hK2⟩⟩ := hall
  refine ⟨max K1 K2, fun n k hk hn hn3 hc hg => ?_⟩
  have hkk : 0 < k * k := Nat.mul_pos hk hk
  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 hm1 : n / n.gcd k ≠ 1 := by
    intro h
    rw [h, Nat.minFac_one] at hg
    omega
  have hm0 : n / n.gcd k ≠ 0 := by
    intro h
    rw [h, Nat.mul_zero] at hnm
    omega
  by_cases hp : (n / n.gcd k).Prime
  · exact le_max_of_le_left
      (hK1 n k _ hk hn hn3 hc hp (lt_of_lt_of_le hg (Nat.minFac_le (Nat.pos_of_ne_zero hm0))) hnm)
  · have hpp : (n / n.gcd k).minFac.Prime := Nat.minFac_prime hm1
    obtain ⟨r, hr⟩ := Nat.minFac_dvd (n / n.gcd k)
    have hr1 : r ≠ 1 := by
      intro h
      rw [h, Nat.mul_one] at hr
      exact hp (hr ▸ hpp)
    have hr0 : r ≠ 0 := by
      intro h
      rw [h, Nat.mul_zero] at hr
      exact hm0 hr
    have hrf : r.minFac > k := by
      have : (n / n.gcd k).minFac ≤ r.minFac :=
        Nat.minFac_le_of_dvd (Nat.minFac_prime hr1).two_le
          (by rw [hr]; exact Dvd.dvd.mul_left (Nat.minFac_dvd r) _)
      omega
    have hrp : r.Prime := by
      by_contra hnr
      have h1 := Nat.minFac_sq_le_self (by omega : 0 < r) hnr
      have h2 : k * k < r.minFac ^ 2 := by
        rw [pow_two]; exact Nat.mul_lt_mul'' hrf hrf
      have h3 : k * (k * k) < (n / n.gcd k).minFac * r := Nat.mul_lt_mul'' hg (by omega)
      have e : k * k * k = k * (k * k) := Nat.mul_assoc _ _ _
      omega
    exact le_max_of_le_right (hK2 n k _ r hk hn hn3 hc hpp hrp hg
      (lt_of_lt_of_le hrf (Nat.minFac_le (by omega))) (by rw [← hr]; exact 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 →