Problems / erdos-849 / variant-72919549
variant-72919549
open
A partial route to the problem.
theorem Opn.erdos_849_three_rows_infinitely_often :
∀ N : ℕ, ∃ a ≥ N, 3 ≤ {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard := 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-72919549».Context
open Nat
/-- Infinitely many integers $a$ are $\binom{n}{k}$ with $1 \le k \le n/2$ in at least three rows
$n$: for every $N$ there is such an $a \ge N$. A consequence of the affirmative answer to
Erdős 849 (it gives one $a$ for each $t \ge 3$, all distinct). The proof uses Singmaster's
Fibonacci family: for $i \ge 1$, $n = F_{2i+2}F_{2i+3}$ and $k = F_{2i}F_{2i+3}$ give
$\binom{n}{k} = \binom{n-1}{k+1}$, and with $\binom{a}{1}$ that is three rows. -/
theorem Opn.erdos_849_three_rows_infinitely_often :
∀ N : ℕ, ∃ a ≥ N, 3 ≤ {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard := 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-72919549/Statement.lean. Origin: variant (partial).
Witness
Not checked — no run on this page records step 7 passing for it.
91498ee03e39.theorem witness : ∃ N : ℕ, 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 →
Relation to the problem’s statement
Checked by the kernel — checked at admission (D-30); no proof of the node is implied.
2c3d11523bb8.-- relation: partial
import Mathlib
theorem relation :
(∀ t ≥ 1, ∃ a : ℕ, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ Nat.choose n k = a}.ncard = t) →
∀ N : ℕ, ∃ a ≥ N, 3 ≤ {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ Nat.choose n k = a}.ncard := by
intro h N
by_contra hc
push_neg at hc
have h' : ∀ t : ℕ, ∃ a : ℕ,
{n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ Nat.choose n k = a}.ncard = t + 3 :=
fun t => h (t + 3) (by omega)
choose f hf using h'
have hlt : ∀ t, f t < N := by
intro t
by_contra hle
push_neg at hle
have := hc (f t) hle
rw [hf t] at this
omega
obtain ⟨x, _, y, _, hne, heq⟩ := Finset.exists_ne_map_eq_of_card_lt_of_maps_to
(s := Finset.range (N + 1)) (t := Finset.range N) (f := f) (by simp)
(fun t _ => Finset.mem_range.mpr (hlt t))
have := hf x
rw [heq, hf y] at this
omegaNo gloss yet: no one has written in words what this relation says (D-3 v3.30); the Lean above is the relation. 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 binomial 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 3 ≤ {n | ∃ k ≥ 1, 2 * k ≤ n ∧ n.choose k = a}.ncard
Deliberate: the statement is 'at least three rows', inclusive; three is the multiplicity the Fibonacci family attains in the k <= n/2 count.
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).