Problems / erdos-849 / variant-3e42e1ad
t = 1 and t = 2 attained infinitely often
variant-3e42e1ad
open
A related variant. not yet signed as pertinent to the target (D-30 v3.12)
$\displaystyle \forall N \in \mathbb{N}:\quad \Bigl(\exists a \ge N,\ \#\bigl\{\, n \in \mathbb{N} : \exists k \ge 1,\ 2k \le n,\ \tbinom{n}{k} = a \,\bigr\} = 1\Bigr) \ \wedge\ \Bigl(\exists a \ge N,\ \#\bigl\{\, n \in \mathbb{N} : \exists k \ge 1,\ 2k \le n,\ \tbinom{n}{k} = a \,\bigr\} = 2\Bigr)$
Here $N$, $a$, $n$, $k$ are natural numbers, and $2k \le n$ is the range $1 \le k \le n/2$ written without division. Each set collects rows $n$ of Pascal's triangle, counted once each; its size is Set.ncard, which is $0$ for an infinite set as well as an empty one (every such set lies in $[2, a]$, the statement spec-38faff03). The two $a$ are chosen separately: the first conjunct has its own $a$, the second its own.
In words: for every $N$ there is some $a \ge N$ that appears as $\binom{n}{k}$ with $1 \le k \le n/2$ in exactly one row, and some $a \ge N$ that appears in exactly two rows. That is, the cases $t = 1$ and $t = 2$ of erdos-849 are each attained by infinitely many $a$.
Lean
theorem Opn.erdos_849_one_and_two_rows_infinitely_often :
∀ N : ℕ, (∃ a ≥ N, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = 1) ∧
(∃ a ≥ N, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = 2) := 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.«variant-3e42e1ad».Context
open Nat
/-- The cases $t = 1$ and $t = 2$ of Erdős 849 each hold for infinitely many $a$: for every $N$
there are $a, b \ge N$ with $a$ in exactly one row and $b$ in exactly two rows (rows $n$ with
$\binom{n}{k} = a$, $1 \le k \le n/2$). The proof takes a prime $a = p$ (only $\binom{p}{1}$) and
$b = \binom{p}{2}$ for a prime $p \ge 7$ (only $\binom{p}{2}$ and $\binom{b}{1}$), since a prime
dividing $\binom{n}{k}$ is at most $n$. -/
theorem Opn.erdos_849_one_and_two_rows_infinitely_often :
∀ N : ℕ, (∃ a ≥ N, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = 1) ∧
(∃ a ≥ N, {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = 2) := 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 t1027e-d, drafted with Claude Fable 5.1 (claude-fable-5-1), 2026-10-27; no one has read it against the Lean and signed it.
Draft · drafted, by the model named above
$\displaystyle \forall N \in \mathbb{N}:\quad \Bigl(\exists a \ge N,\ \#\bigl\{\, n \in \mathbb{N} : \exists k \ge 1,\ 2k \le n,\ \tbinom{n}{k} = a \,\bigr\} = 1\Bigr) \ \wedge\ \Bigl(\exists a \ge N,\ \#\bigl\{\, n \in \mathbb{N} : \exists k \ge 1,\ 2k \le n,\ \tbinom{n}{k} = a \,\bigr\} = 2\Bigr)$
Here $N$, $a$, $n$, $k$ are natural numbers, and $2k \le n$ is the range $1 \le k \le n/2$ written without division. Each set collects rows $n$ of Pascal's triangle, counted once each; its size is Set.ncard, which is $0$ for an infinite set as well as an empty one (every such set lies in $[2, a]$, the statement spec-38faff03). The two $a$ are chosen separately: the first conjunct has its own $a$, the second its own.
In words: for every $N$ there is some $a \ge N$ that appears as $\binom{n}{k}$ with $1 \le k \le n/2$ in exactly one row, and some $a \ge N$ that appears in exactly two rows. That is, the cases $t = 1$ and $t = 2$ of erdos-849 are each attained by infinitely many $a$.
Rendered from gloss/ed6974acabc5….md · Improve these words →
Rendered from targets/erdos-849/nodes/variant-3e42e1ad/Statement.lean. Origin: variant (related).
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 →
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 binomial 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).