Problems / erdos-1094 / erdos-1094--h2--h1--h4
the thin strip above k²
erdos-1094--h2--h1--h4
open
Hole h_strip of erdos-1094--h2--h1 (split by 20261014T075000Z-t1014-a-partial.lean).
$\displaystyle \exists K\in\mathbb N\ \forall n,k\in\mathbb N:\ 0<k,\ k^2\le n,\ n<k\bigl(k+3k^{21/40}\bigr),\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$
In words: only finitely many $k$ admit an $n$ in the strip $k^2\le n<k(k+3k^{0.525})$ (the inequality is taken over the reals, with $21/40$ a real exponent) such that $k\cdot\lfloor n/k\rfloor$ divides $k!$ and the least prime factor of $\binom nk$ exceeds $\lfloor n/k\rfloor$.
Lean conventions: n / k is floor division; Nat.minFac is 1 at 1 (and 2 at 0); 0 < k is a hypothesis.
Lean
theorem erdos_1094__h2__h1__h4 : ∃ (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 → k ≤ K := by
sorryWhy 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.
Proved from this hole by 20261014T111658Z-t1014-y-partial.lean (merged in d14c9e52445b, attestation 000515).
h_gp→ erdos-1094--h2--h1--h4--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,\ \ \frac{n}{\gcd(n,k)}\text{ prime}\ \Longrightarrow\ k\le K$
Read the partial proof (Lean)
theorem erdos_1094__h2__h1__h4 : ∃ (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 → k ≤ K := by
-- Proved here (assembly): under k*k ≤ n and minFac C(n,k) > n/k, the number n / gcd(n,k) is prime.
-- Reason: n/gcd(n,k) divides C(n,k) (from k*C(n,k) = n*C(n-1,k-1) and coprimality), so all its
-- prime factors exceed n/k ≥ k; a composite would be ≥ (n/k+1)^2 > n.
have h_gcd_prime : ∀ (n k : ℕ), 0 < k → k * k ≤ n → (n.choose k).minFac > n / k →
(n / n.gcd k).Prime := by
intro n k hk hn hm
have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn
have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn
have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
set g := n.gcd k with hg
have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
have hgn : g ∣ n := Nat.gcd_dvd_left n k
have hgk : g ∣ k := Nat.gcd_dvd_right n k
-- k * C(n,k) = n * C(n-1,k-1)
have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by
have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
have hdvd : n / g ∣ n.choose k := by
have h1 : n / g ∣ n.choose k * (k / g) := by
refine ⟨(n - 1).choose (k - 1), ?_⟩
have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by
rw [← e1, ← e2]; exact hid
have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by
linear_combination this
exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
exact hcop.dvd_of_dvd_mul_right h1
have hCpos : 0 < n.choose k := Nat.choose_pos hkn
-- n/g ≥ n/k ≥ k ≥ 1
have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
by_contra hnp
have h2 : 2 ≤ n / g := by
rcases Nat.lt_or_ge (n / g) 2 with h | h
· -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n
exfalso
have hk1 : k ≤ 1 := by omega
have hk1' : k = 1 := by omega
subst hk1'
have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega)
have hn1 : n = 1 := by omega
subst hn1
simp at hm
· exact h
-- q := minFac (n/g); q ∣ C so minFac C ≤ q
have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
have hqC : (n.choose k).minFac ≤ (n / g).minFac :=
Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp
have hq : n / k + 1 ≤ (n / g).minFac := by omega
have hng' : n / g ≤ n := Nat.div_le_self n g
have hlt : n < (n / k + 1) * k := by
have := Nat.lt_mul_div_succ n hk
linarith [this]
have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega)
nlinarith
-- The open half: the same statement, given in addition that n / gcd(n,k) is prime.
have h_gp : ∃ (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 / n.gcd k).Prime → k ≤ K := by
sorry
obtain ⟨K, hK⟩ := h_gp
refine ⟨K, fun n k hk hn he hd hm => hK n k hk hn he hd hm ?_⟩
exact h_gcd_prime n k hk hn hmThe 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/attempts/20261014T111658Z-t1014-y-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
Literature: Known: a proof is published and not formalised · proposed by t1014-z, awaiting a steward or curator
References and summary
Proposed by t1014-z, awaiting a steward or curator: Known: a proof is published and not formalised (record, 2026-10-14T11:20:02Z).
- S. V. Konyagin, Estimates of the least prime factor of a binomial coefficient, Mathematika 46 (1999) 41-55 — g(k) >= exp(c (log k)^2) for large k; cited through the existing literature proposals on erdos-1094--h2--h1 and --h2--h1--h1 and erdosproblems.com/1095, not read in the original by me
- Literature proposal on erdos-1094--h2--h1--h1 (t1009-c, 2026-10-09) — that node (no n in [2k, k^3) with every prime factor of C(n,k) above k, large k) implies this one directly
Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.
Untrusted: summary by t1014-z, drafted with Claude Opus 5.5 (claude-opus-5-5) through Claude Code, tester C. Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h4/literature/20261014T112002Z-t1014-z.yaml.
This node covers k^2 <= n < k(k + 3k^0.525) with k(n/k) | k! and minFac C(n,k) > n/k. Since n >= k^2 gives n/k >= k, the hypothesis says every prime factor of C(n,k) exceeds k, and n < k(k+3k^0.525) < k^3 for k beyond a small bound; so the node follows from erdos-1094--h2--h1--h1 (Konyagin's bound g(k) > k^3 for large k) without using the divisibility hypothesis. The deduction is mine and unchecked; the record is the same published input as --h2--h1--h1, not a separate theorem. Nothing is formalised.
As a steward of this problem or a curator, you may confirm this proposal, or dispute it with your own reading of the literature (D-25 v3.45).
- erdos-1094--h2--h1--h4 · Known: a proof is published and not formalised · proposed by
t1014-z· 2026-10-14T11:20:02Z · record
Work on it
How to contribute → · Pull requests in flight ↗ · See it in the problem’s graph →
Record
Statement: the Lean file and its words (2 versions)
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».Context
open scoped Nat
/-! Hole `h_strip` 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 : ∃ (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 → k ≤ K := by
sorryA 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 t1014-y, drafted with claude-opus-5-5 via Claude Code, 2026-10-14; 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:\ 0<k,\ k^2\le n,\ n<k\bigl(k+3k^{21/40}\bigr),\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$
In words: only finitely many $k$ admit an $n$ in the strip $k^2\le n<k(k+3k^{0.525})$ (the inequality is taken over the reals, with $21/40$ a real exponent) such that $k\cdot\lfloor n/k\rfloor$ divides $k!$ and the least prime factor of $\binom nk$ exceeds $\lfloor n/k\rfloor$.
Lean conventions: n / k is floor division; Nat.minFac is 1 at 1 (and 2 at 0); 0 < k is a hypothesis.
Rendered from gloss/39e8ada24190….md · Improve these words →
History: 2 versions on record
2026-10-14 · written by t1014-y, drafted with claude-opus-5-5 via Claude Code · not signed · gloss/39e8ada24190….md · the first version of its chain
Read this version
$\displaystyle \exists K\in\mathbb N\ \forall n,k\in\mathbb N:\ 0<k,\ k^2\le n,\ n<k\bigl(k+3k^{21/40}\bigr),\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$
In words: only finitely many $k$ admit an $n$ in the strip $k^2\le n<k(k+3k^{0.525})$ (the inequality is taken over the reals, with $21/40$ a real exponent) such that $k\cdot\lfloor n/k\rfloor$ divides $k!$ and the least prime factor of $\binom nk$ exceeds $\lfloor n/k\rfloor$.
Lean conventions:
n / kis floor division;Nat.minFacis 1 at 1 (and 2 at 0);0 < kis a hypothesis.2026-10-18 · written by f29-words, drafted with Claude Fable 5.1 (claude-fable-5-1) · not signed · current · gloss/44aa9a3d6c7b….md · diff to its predecessor
Read this version
$\displaystyle \exists K\in\mathbb N\ \forall n,k\in\mathbb N:\ 0<k,\ k^2\le n,\ n<k\bigl(k+3k^{21/40}\bigr),\ k\lfloor n/k\rfloor \mid k!,\ \operatorname{minFac}\binom nk>\lfloor n/k\rfloor\ \Longrightarrow\ k\le K.$
In words: only finitely many $k$ admit an $n$ in the strip $k^2\le n<k(k+3k^{0.525})$ (the inequality is taken over the reals, with $21/40$ a real exponent) such that $k\cdot\lfloor n/k\rfloor$ divides $k!$ and the least prime factor of $\binom nk$ exceeds $\lfloor n/k\rfloor$.
Lean conventions:
n / kis floor division;Nat.minFacis 1 at 1 (and 2 at 0);0 < kis a hypothesis.
Diff of 44aa9a3d6c7b against 39e8ada24190
(the words are the same)
Improve these words → Nothing is edited: a correction is a new version, and every version stays on the record (D-3 v3.30).
Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h4/Statement.lean. Origin: skeleton-hole.
Depends on (1), each in words
Depends on, each in words where someone has written them:
- erdos-1094--h2--h1--h4--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,\ \ \frac{n}{\gcd(n,k)}\text{ prime}\ \Longrightarrow\ k\le K$
Attestation: none of a proof
No proof of this statement has been merged. A partial assembly merged under attestations/000515.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.
1aa8a1c1b9f3.import Mathlib open scoped Nat 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 (1)
1 recorded. Routes refuted: none. Failure classes: none.
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 t1014-y; merged in d14c9e52445b under attestations/000515.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/attempts/20261014T111658Z-t1014-y-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 20261014T111658Z-t1014-y-partial.lean, extracted by the gate at f97b6921b55b 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_gcd_primehave∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd 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 → k ≤ K, withh_gcd_prime : ∀ (n k : ℕ), (0 : ℕ) < k → k * k ≤ n → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k).Lean, lines 18–71
have h_gcd_prime : ∀ (n k : ℕ), 0 < k → k * k ≤ n → (n.choose k).minFac > n / k → (n / n.gcd k).Prime := by intro n k hk hn hm have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn set g := n.gcd k with hg have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0 have hgn : g ∣ n := Nat.gcd_dvd_left n k have hgk : g ∣ k := Nat.gcd_dvd_right n k -- k * C(n,k) = n * C(n-1,k-1) have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by have := Nat.add_one_mul_choose_eq (n - 1) (k - 1) rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0 have hdvd : n / g ∣ n.choose k := by have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm exact hcop.dvd_of_dvd_mul_right h1 have hCpos : 0 < n.choose k := Nat.choose_pos hkn -- n/g ≥ n/k ≥ k ≥ 1 have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0 by_contra hnp have h2 : 2 ≤ n / g := by rcases Nat.lt_or_ge (n / g) 2 with h | h · -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n exfalso have hk1 : k ≤ 1 := by omega have hk1' : k = 1 := by omega subst hk1' have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega) have hn1 : n = 1 := by omega subst hn1 simp at hm · exact h -- q := minFac (n/g); q ∣ C so minFac C ≤ q have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le have hqC : (n.choose k).minFac ≤ (n / g).minFac := Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd) have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp have hq : n / k + 1 ≤ (n / g).minFac := by omega have hng' : n / g ≤ n := Nat.div_le_self n g have hlt : n < (n / k + 1) * k := by have := Nat.lt_mul_div_succ n hk linarith [this] have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega) nlinarithh_gcd_prime.hn0have(0 : ℕ) < nLeaves
Nat.Prime (n / n.gcd k), withhn0 : (0 : ℕ) < n.Uses library
lt_of_lt_of_le,Nat.mul_pos.Lean, line 21
have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn
h_gcd_prime.hknhavek ≤ nLeaves
Nat.Prime (n / n.gcd k), withhkn : k ≤ n.Uses library
le_transThe relation≤on a preorder is transitive. ,Nat.le_mul_of_pos_left.Lean, line 22
have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn
h_gcd_prime.hkmhavek ≤ n / kLeaves
Nat.Prime (n / n.gcd k), withhkm : k ≤ n / k.Uses library
Nat.le_div_iff_mul_le.Lean, line 23
have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
h_gcd_prime.hg0have(0 : ℕ) < gLeaves
Nat.Prime (n / g), withhg0 : (0 : ℕ) < g.Uses library
Nat.gcd_pos_of_pos_left.Lean, line 25
have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
h_gcd_prime.hgnhaveg ∣ nLeaves
Nat.Prime (n / g), withhgn : g ∣ n.Uses library
Nat.gcd_dvd_left.Lean, line 26
have hgn : g ∣ n := Nat.gcd_dvd_left n k
h_gcd_prime.hgkhaveg ∣ kLeaves
Nat.Prime (n / g), withhgk : g ∣ k.Uses library
Nat.gcd_dvd_right.Lean, line 27
have hgk : g ∣ k := Nat.gcd_dvd_right n k
h_gcd_prime.hidhaven * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * kLeaves
Nat.Prime (n / g), withhid : n * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * k.Uses library
Nat.sub_add_cancel.Lean, lines 29–31
have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by have := Nat.add_one_mul_choose_eq (n - 1) (k - 1) rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at thish_gcd_prime.hid.thishave(n - (1 : ℕ) + (1 : ℕ)) * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = (n - (1 : ℕ) + (1 : ℕ)).choose (k - (1 : ℕ) + (1 : ℕ)) * (k - (1 : ℕ) + (1 : ℕ))Leaves
n * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * k, withthis : (n - (1 : ℕ) + (1 : ℕ)) * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = (n - (1 : ℕ) + (1 : ℕ)).choose (k - (1 : ℕ) + (1 : ℕ)) * (k - (1 : ℕ) + (1 : ℕ)).Uses library
Nat.add_one_mul_choose_eq.Lean, line 30
have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
h_gcd_prime.hcophave(n / g).Coprime (k / g)Leaves
Nat.Prime (n / g), withhcop : (n / g).Coprime (k / g).Uses library
Nat.Coprimemandnare coprime, or relatively prime, if theirgcdis 1. ,Nat.coprime_div_gcd_div_gcd.Lean, line 32
have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
h_gcd_prime.hdvdhaven / g ∣ n.choose kLeaves
Nat.Prime (n / g), withhdvd : n / g ∣ n.choose k.Lean, lines 33–43
have hdvd : n / g ∣ n.choose k := by have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm exact hcop.dvd_of_dvd_mul_right h1h_gcd_prime.hdvd.h1haven / g ∣ n.choose k * (k / g)Leaves
n / g ∣ n.choose k, withh1 : n / g ∣ n.choose k * (k / g).Uses library
Exists.introExistential introduction. ,Nat.eq_of_mul_eq_mul_right.Lean, lines 34–42
have h1 : n / g ∣ n.choose k * (k / g) := by refine ⟨(n - 1).choose (k - 1), ?_⟩ have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hid have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this exact (Nat.eq_of_mul_eq_mul_right hg0 this).symmh_gcd_prime.hdvd.h1.e1haven = n / g * gLeaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withe1 : n = n / g * g.Uses library
Nat.div_mul_cancel.Lean, line 36
have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
h_gcd_prime.hdvd.h1.e2havek = k / g * gLeaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withe2 : k = k / g * g.Uses library
Nat.div_mul_cancel.Lean, line 37
have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
h_gcd_prime.hdvd.h1.s3haven / g * g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * (k / g * g)Leaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withthis : n / g * g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) = n.choose k * (k / g * g).Lean, lines 38–39
have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by rw [← e1, ← e2]; exact hidh_gcd_prime.hdvd.h1.s4haven / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) * g = n.choose k * (k / g) * gLeaves
n.choose k * (k / g) = n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)), withthis : n / g * (n - (1 : ℕ)).choose (k - (1 : ℕ)) * g = n.choose k * (k / g) * g.Lean, lines 40–41
have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by linear_combination this
h_gcd_prime.hCposhave(0 : ℕ) < n.choose kLeaves
Nat.Prime (n / g), withhCpos : (0 : ℕ) < n.choose k.Uses library
Nat.choose_pos.Lean, line 44
have hCpos : 0 < n.choose k := Nat.choose_pos hkn
h_gcd_prime.hnghaven / k ≤ n / gLeaves
Nat.Prime (n / g), withhng : n / k ≤ n / g.Uses library
Nat.div_le_div_left,Nat.le_of_dvd.Lean, line 46
have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
h_gcd_prime.h2have(2 : ℕ) ≤ n / gLeaves
False, withh2 : (2 : ℕ) ≤ n / g.Uses library
Nat.lt_or_ge.Lean, lines 48–59
have h2 : 2 ≤ n / g := by rcases Nat.lt_or_ge (n / g) 2 with h | h · -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n exfalso have hk1 : k ≤ 1 := by omega have hk1' : k = 1 := by omega subst hk1' have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega) have hn1 : n = 1 := by omega subst hn1 simp at hm · exact hh_gcd_prime.h2.s1caseLeaves
(2 : ℕ) ≤ n / g, withh : n / g < (2 : ℕ).Lean, lines 50–58
· -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n exfalso have hk1 : k ≤ 1 := by omega have hk1' : k = 1 := by omega subst hk1' have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega) have hn1 : n = 1 := by omega subst hn1 simp at hmh_gcd_prime.h2.s1.hk1havek ≤ (1 : ℕ)routine: omegaLeaves
False, withhk1 : k ≤ (1 : ℕ).Lean, line 52
have hk1 : k ≤ 1 := by omega
h_gcd_prime.h2.s1.hk1'havek = (1 : ℕ)routine: omegaLeaves
False, withhk1' : k = (1 : ℕ).Lean, line 53
have hk1' : k = 1 := by omega
h_gcd_prime.h2.s1.thishaven ≤ (1 : ℕ)Leaves
False, withthis : n ≤ (1 : ℕ).Lean, line 55
have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega)
h_gcd_prime.h2.s1.hn1haven = (1 : ℕ)routine: omegaLeaves
False, withhn1 : n = (1 : ℕ).Lean, line 56
have hn1 : n = 1 := by omega
h_gcd_prime.h2.s2caseLeaves
(2 : ℕ) ≤ n / g, withh : n / g ≥ (2 : ℕ).
h_gcd_prime.hq2have(2 : ℕ) ≤ (n / g).minFacLeaves
False, withhq2 : (2 : ℕ) ≤ (n / g).minFac.Uses library
Nat.minFac_prime.Lean, line 61
have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
h_gcd_prime.hqChave(n.choose k).minFac ≤ (n / g).minFacLeaves
False, withhqC : (n.choose k).minFac ≤ (n / g).minFac.Uses library
Nat.minFac_le_of_dvd,Nat.minFac_dvd.Lean, lines 62–63
have hqC : (n.choose k).minFac ≤ (n / g).minFac := Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)h_gcd_prime.hsqhave(n / g).minFac ^ (2 : ℕ) ≤ n / gLeaves
False, withhsq : (n / g).minFac ^ (2 : ℕ) ≤ n / g.Uses library
Nat.minFac_sq_le_selfThe square of the smallest prime factor of a composite numbernis at mostn. .Lean, line 64
have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp
h_gcd_prime.hqhaven / k + (1 : ℕ) ≤ (n / g).minFacroutine: omegaLeaves
False, withhq : n / k + (1 : ℕ) ≤ (n / g).minFac.Lean, line 65
have hq : n / k + 1 ≤ (n / g).minFac := by omega
h_gcd_prime.hng'haven / g ≤ nLeaves
False, withhng' : n / g ≤ n.Uses library
Nat.div_le_self.Lean, line 66
have hng' : n / g ≤ n := Nat.div_le_self n g
h_gcd_prime.hlthaven < (n / k + (1 : ℕ)) * kLeaves
False, withhlt : n < (n / k + (1 : ℕ)) * k.Lean, lines 67–69
have hlt : n < (n / k + 1) * k := by have := Nat.lt_mul_div_succ n hk linarith [this]h_gcd_prime.hlt.thishaven < k * (n / k + (1 : ℕ))Leaves
n < (n / k + (1 : ℕ)) * k, withthis : n < k * (n / k + (1 : ℕ)).Uses library
Nat.lt_mul_div_succ.Lean, line 68
have := Nat.lt_mul_div_succ n hk
h_gcd_prime.thishave(n / k + (1 : ℕ)) * k ≤ (n / k + (1 : ℕ)) * (n / k + (1 : ℕ))Leaves
False, withthis : (n / k + (1 : ℕ)) * k ≤ (n / k + (1 : ℕ)) * (n / k + (1 : ℕ)).Uses library
Nat.mul_le_mul_left.Lean, line 70
have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega)
h_gphole∃ (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 ≤ KholeLeaves
∃ (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 → k ≤ K, withh_gp : ∃ (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.Left open as a hole; its statement is erdos-1094--h2--h1--h4--h1 (open).
Lean, lines 73–79
have h_gp : ∃ (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 / n.gcd k).Prime → k ≤ K := by sorrys3obtain∃ (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 ≤ KLeaves
∃ (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 → k ≤ K, withK : ℕ,hK : ∀ (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.Lean, line 80
obtain ⟨K, hK⟩ := h_gp
closeterm∃ (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 → k ≤ KCloses the goal.
Uses library
Exists.introExistential introduction. .Lean, lines 81–82
refine ⟨K, fun n k hk hn he hd hm => hK n k hk hn he hd hm ?_⟩ exact h_gcd_prime n k hk hn hm
import Mathlib
import Nodes.«erdos-1094--h2--h1--h4».Context
open scoped Nat
/-! Hole `h_strip` 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 : ∃ (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 → k ≤ K := by
-- Proved here (assembly): under k*k ≤ n and minFac C(n,k) > n/k, the number n / gcd(n,k) is prime.
-- Reason: n/gcd(n,k) divides C(n,k) (from k*C(n,k) = n*C(n-1,k-1) and coprimality), so all its
-- prime factors exceed n/k ≥ k; a composite would be ≥ (n/k+1)^2 > n.
have h_gcd_prime : ∀ (n k : ℕ), 0 < k → k * k ≤ n → (n.choose k).minFac > n / k →
(n / n.gcd k).Prime := by
intro n k hk hn hm
have hn0 : 0 < n := lt_of_lt_of_le (Nat.mul_pos hk hk) hn
have hkn : k ≤ n := le_trans (Nat.le_mul_of_pos_left k hk) hn
have hkm : k ≤ n / k := (Nat.le_div_iff_mul_le hk).2 hn
set g := n.gcd k with hg
have hg0 : 0 < g := Nat.gcd_pos_of_pos_left k hn0
have hgn : g ∣ n := Nat.gcd_dvd_left n k
have hgk : g ∣ k := Nat.gcd_dvd_right n k
-- k * C(n,k) = n * C(n-1,k-1)
have hid : n * (n - 1).choose (k - 1) = n.choose k * k := by
have := Nat.add_one_mul_choose_eq (n - 1) (k - 1)
rwa [Nat.sub_add_cancel (by omega : 1 ≤ n), Nat.sub_add_cancel (by omega : 1 ≤ k)] at this
have hcop : Nat.Coprime (n / g) (k / g) := Nat.coprime_div_gcd_div_gcd hg0
have hdvd : n / g ∣ n.choose k := by
have h1 : n / g ∣ n.choose k * (k / g) := by
refine ⟨(n - 1).choose (k - 1), ?_⟩
have e1 : n = n / g * g := (Nat.div_mul_cancel hgn).symm
have e2 : k = k / g * g := (Nat.div_mul_cancel hgk).symm
have : n / g * g * (n - 1).choose (k - 1) = n.choose k * (k / g * g) := by
rw [← e1, ← e2]; exact hid
have : (n / g * (n - 1).choose (k - 1)) * g = (n.choose k * (k / g)) * g := by
linear_combination this
exact (Nat.eq_of_mul_eq_mul_right hg0 this).symm
exact hcop.dvd_of_dvd_mul_right h1
have hCpos : 0 < n.choose k := Nat.choose_pos hkn
-- n/g ≥ n/k ≥ k ≥ 1
have hng : n / k ≤ n / g := Nat.div_le_div_left (Nat.le_of_dvd hk hgk) hg0
by_contra hnp
have h2 : 2 ≤ n / g := by
rcases Nat.lt_or_ge (n / g) 2 with h | h
· -- n/g ≤ 1 so n/k ≤ 1 so k = 1, n/k = n
exfalso
have hk1 : k ≤ 1 := by omega
have hk1' : k = 1 := by omega
subst hk1'
have : n ≤ 1 := by simpa using (show n / 1 ≤ 1 by omega)
have hn1 : n = 1 := by omega
subst hn1
simp at hm
· exact h
-- q := minFac (n/g); q ∣ C so minFac C ≤ q
have hq2 : 2 ≤ (n / g).minFac := (Nat.minFac_prime (by omega)).two_le
have hqC : (n.choose k).minFac ≤ (n / g).minFac :=
Nat.minFac_le_of_dvd hq2 ((Nat.minFac_dvd _).trans hdvd)
have hsq : (n / g).minFac ^ 2 ≤ n / g := Nat.minFac_sq_le_self (by omega) hnp
have hq : n / k + 1 ≤ (n / g).minFac := by omega
have hng' : n / g ≤ n := Nat.div_le_self n g
have hlt : n < (n / k + 1) * k := by
have := Nat.lt_mul_div_succ n hk
linarith [this]
have : (n / k + 1) * k ≤ (n / k + 1) * (n / k + 1) := Nat.mul_le_mul_left _ (by omega)
nlinarith
-- The open half: the same statement, given in addition that n / gcd(n,k) is prime.
have h_gp : ∃ (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 / n.gcd k).Prime → k ≤ K := by
sorry
obtain ⟨K, hK⟩ := h_gp
refine ⟨K, fun n k hk hn he hd hm => hK n k hk hn he hd hm ?_⟩
exact h_gcd_prime n k hk hn hmHow 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).