Problems / erdos-1094 / erdos-1094--h3--h2--h1--h1
EES bound below k squared
erdos-1094--h3--h2--h1--h1
needs a witness: nothing else blocks it, and supplying one is the work (propose it through /proposals/witness)
Hole h_lt of erdos-1094--h3--h2--h1 (split by 20261018T193200Z-t1018-c-partial.lean).
$\displaystyle \exists c>0\,\exists K\,\forall n,k:\ K<k,\ 2k\le n<k^2,\ \mathrm{lpf}\binom{n}{k}>k \Rightarrow k^{1+c}<n$
The Ecklund–Erdős–Selfridge bound restricted to the only range where it has content.
Lean
theorem erdos_1094__h3__h2__h1__h1 : ∃ (c : ℝ),
(0 : ℝ) < c ∧
∃ (K : ℕ),
∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := 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
Needs a witness: nothing else blocks it, and supplying one is the work (propose it through /proposals/witness).
What is known
Work on it
Supply a witness → Its slot is open; the witness is in the record below.
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--h3--h2--h1--h1».Context
open scoped Nat
/-! Hole `h_lt` 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__h3__h2__h1__h1 : ∃ (c : ℝ),
(0 : ℝ) < c ∧
∃ (K : ℕ),
∀ (n k : ℕ), K < k → (2 : ℕ) * k ≤ n → n < k * k → (n.choose k).minFac > k → (↑k : ℝ) ^ ((1 : ℝ) + c) < (↑n : ℝ) := 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-c, 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 c>0\,\exists K\,\forall n,k:\ K<k,\ 2k\le n<k^2,\ \mathrm{lpf}\binom{n}{k}>k \Rightarrow k^{1+c}<n$
The Ecklund–Erdős–Selfridge bound restricted to the only range where it has content.
Rendered from gloss/c3f009acde77….md · Improve these words →
Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2--h1--h1/Statement.lean. Origin: compiler-derived.
Witness — its slot is open
Not checked — the witness slot is open.
/proposals/witness. Rendered from targets/erdos-1094/nodes/erdos-1094--h3--h2--h1--h1/Witness.lean, sha256 f00db10e8f09.import Mathlib import Nodes.«erdos-1094--h3--h2--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 := by sorry
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).