Problems / erdos-849 / variant-a30f5217
variant-a30f5217
open
A related variant. not yet signed as pertinent to the target (D-30 v3.12)
theorem Opn.erdos_849_rows_ncard_le_log : ∀ a : ℕ,
{n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard ≤ Nat.log 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.«variant-a30f5217».Context
open Nat
/-- Erdős 849, the elementary upper bound on multiplicity (the half-triangle form of
Singmaster's 1971 bound `N(a) = O(log a)`): the number of rows `n` in which `a` appears as
`C(n, k)` with `1 ≤ k ≤ n/2` is at most `⌊log₂ a⌋`. Each `k` gives at most one row, since
`C(·, k)` is strictly increasing, and a row with `C(n, k) = a` has `2^k ≤ C(2k, k) ≤ a`. -/
theorem Opn.erdos_849_rows_ncard_le_log : ∀ a : ℕ,
{n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard ≤ Nat.log 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/variant-a30f5217/Statement.lean. Origin: variant (related).
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 (1)
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.
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).