Problems / erdos-1094 / erdos-1094--h2--h2--h3--h1--h1
beyond van Doorn–Tang, n/gcd(n,k) prime, k ∤ n
erdos-1094--h2--h2--h3--h1--h1
open
Hole h_ndvd of erdos-1094--h2--h2--h3--h1 (split by 20261015T144930Z-t1015c-a08-partial.lean).
$\displaystyle \exists K\in\mathbb{N}\ \forall n,k\in\mathbb{N}:\quad 0<k,\ \ k^3\le n,\ \ \exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)<n+1,\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ k\nmid n\ \Longrightarrow\ k\le K$
Only finitely many $k$ admit an $n$ with $n\ge k^3$ and $n+1>\exp\bigl((\log k)^2/(20\log\log k)\bigr)$ (natural logarithms, over the reals) 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 with $k\nmid n$. Lean conventions: n / k is floor division, $n/\gcd(n,k)$ is natural-number division, exact here since the gcd divides $n$, Nat.minFac is the least prime factor (1 at 1, 2 at 0), and Real.log is 0 at 0, so for small $k$ the exponent is a junk value ($\log\log 1=0$ and division by 0 gives 0).
Lean
theorem erdos_1094__h2__h2__h3__h1__h1 : ∃ (K : ℕ),
∀ (n k : ℕ),
(0 : ℕ) < k →
k * k * k ≤ n →
Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ) →
k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → ¬k ∣ n → 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 closes it.
What is known
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 (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--h2--h3--h1--h1».Context
open scoped Nat
/-! Hole `h_ndvd` 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__h2__h3__h1__h1 : ∃ (K : ℕ),
∀ (n k : ℕ),
(0 : ℕ) < k →
k * k * k ≤ n →
Real.exp (Real.log (↑k : ℝ) ^ (2 : ℕ) / ((20 : ℝ) * Real.log (Real.log (↑k : ℝ)))) < (↑n : ℝ) + (1 : ℝ) →
k * (n / k) ∣ k.factorial → (n.choose k).minFac > n / k → Nat.Prime (n / n.gcd k) → ¬k ∣ n → 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 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^3\le n,\ \ \exp\!\Bigl(\frac{(\log k)^2}{20\log\log k}\Bigr)<n+1,\ \ k\lfloor n/k\rfloor\mid k!,\ \ \operatorname{minFac}\tbinom{n}{k}>\lfloor n/k\rfloor,\ \ \frac{n}{\gcd(n,k)}\text{ prime},\ \ k\nmid n\ \Longrightarrow\ k\le K$
Only finitely many $k$ admit an $n$ with $n\ge k^3$ and $n+1>\exp\bigl((\log k)^2/(20\log\log k)\bigr)$ (natural logarithms, over the reals) 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 with $k\nmid n$. Lean conventions: n / k is floor division, $n/\gcd(n,k)$ is natural-number division, exact here since the gcd divides $n$, Nat.minFac is the least prime factor (1 at 1, 2 at 0), and Real.log is 0 at 0, so for small $k$ the exponent is a junk value ($\log\log 1=0$ and division by 0 gives 0).
Rendered from gloss/13a8f739a3da….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h2--h3--h1--h1/Statement.lean. Origin: compiler-derived.
Witness
Not checked — no run on this page records step 7 passing for it.
d610aa356d48.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 →
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).