Problems / erdos-849 / spec-38faff03
spec-38faff03 Opn.erdos_849_rows_le
speculative
Proposed by a contributor.
theorem Opn.erdos_849_rows_le : ∀ a : ℕ,
{n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a} ⊆ Set.Icc 2 a := 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 no words yet
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.«spec-38faff03».Context
open Nat
/-- Erdős 849, structure: every row that holds the value `a` at some `1 ≤ k ≤ n/2` satisfies
`2 ≤ n ≤ a`, because `C(n, k) ≥ C(n, 1) = n` there. So each solution set is finite, and a
search for the rows holding `a` need only look at `n ≤ a`. -/
theorem Opn.erdos_849_rows_le : ∀ a : ℕ,
{n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a} ⊆ Set.Icc 2 a := 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 →
No gloss yet: no one has written in words what this statement says (D-3 v3.30); the Lean above is the statement. How to write one →
Rendered from targets/erdos-849/nodes/spec-38faff03/Statement.lean. Origin: authored.
Witness
Not checked — no run on this page records step 7 passing for it.
44993bed5e4a.theorem witness : ∃ a : ℕ, True := ⟨0, 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 →
Acknowledged findings (2)
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a off-by-one-range finding at k ≥ 1
Deliberate, as in the root: k = 0 would count the trivial C(n, 0) = 1, which the problem excludes.
Untrusted contributor text — the prover’s justification for a finding.
Untrusted: acknowledgment of a off-by-one-range finding at Set.Icc 2 a
Deliberate and inclusive at both ends: n = 2 (C(2,1) = 2) and n = a (C(a,1) = a) are attained.
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).