Problems / erdos-1094 / erdos-1094--h2--h1--h4--h1--h2--h1
proper common divisor case
erdos-1094--h2--h1--h4--h1--h2--h1
open
Hole h_proper of erdos-1094--h2--h1--h4--h1--h2 (split by 20261018T192800Z-t1018-b-partial.lean).
$\displaystyle \exists K\ \forall n,k:\ \text{(the node's hypotheses)} \wedge 2 \le \gcd(n,k) < k \Rightarrow k \le K$
The case gcd(n,k) = k is closed in the assembly. When gcd(n,k) = k, k ∣ n, so n/k = q is prime and k·q = n ∣ k!, giving q ≤ k; with k² ≤ n, q = k, so k is prime and k² ∣ k!, i.e. k ∣ (k-1)!, impossible. Only proper divisors 2 ≤ gcd(n,k) < k remain.
Lean
theorem erdos_1094__h2__h1__h4__h1__h2__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) → (2 : ℕ) ≤ n.gcd k → n.gcd k < 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 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--h1--h4--h1--h2--h1».Context
open scoped Nat
/-! Hole `h_proper` 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__h2__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) → (2 : ℕ) ≤ n.gcd k → n.gcd k < 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 t1018-b, drafted with claude-opus-5-5, 2026-10-18; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \exists K\ \forall n,k:\ \text{(the node's hypotheses)} \wedge 2 \le \gcd(n,k) < k \Rightarrow k \le K$
The case gcd(n,k) = k is closed in the assembly. When gcd(n,k) = k, k ∣ n, so n/k = q is prime and k·q = n ∣ k!, giving q ≤ k; with k² ≤ n, q = k, so k is prime and k² ∣ k!, i.e. k ∣ (k-1)!, impossible. Only proper divisors 2 ≤ gcd(n,k) < k remain.
Rendered from gloss/9424bb3678c4….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h2--h1--h4--h1--h2--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).