Open Proof Network

Problems / erdos-849

erdos-849

open Listed, and its statements accept work. statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only review: needs an intent signer · 2 candidates, 2 clusters, 13 questions waiting

Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions?

Erdős problem 849: Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions? Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/849

ProvedExplainedWritten up

This problem is open for work. How to contribute →

Statements

10 statements. The problem's own statement is the one selected when the page opens. A statement is drawn above the statements it depends on, so the pieces of its proof are below it and a variant that uses it is above it. Select one to see its record.

proved A proof passed all nine checks and was merged. Proved is not the same as explained. protocol: proved open No proof has closed this statement and nothing blocks starting on it. Anyone may work on it now. protocol: ready · on the frontier blocked Waits on other statements, or on a definition that has not been checked yet. Not accepting work. A statement waiting only for its witness is not blocked in this sense: it needs a witness. protocol: blocked any one route closes it A diamond under a statement that two or more routes, or a resolving variant, could close: any one of them suffices (OR), and so would a direct proof. protocol: routes (D-25 v3.40) a weaker version of the problem A dashed line from a variant up into the problem's own statement: the variant's Relation.lean, checked by the gate at admission, proves that the problem implies the variant, so the variant is a weaker version of it and a proof of it is partial progress, never a proof of the problem. protocol: relation: partial (D-30) speculative statement A statement not connected to the problem: a speculative statement proposed for it (or its revision), or a related variant, with its own holes, in the column at the right of the drawing. No line joins it to the tree at rest: hover or select it to light the lines the record has measured from it (a proof that uses it, a lemma, a relation). Everything connected to the problem, variants with a checked relation included, is in the tree; a statement lives in one place, never both. protocol: proposed-for record (D-14 v3.26, v3.46) open, proposed Literature: Open problem: no proof is known — proposed by a contributor, awaiting a steward or curator. A fact about the literature, never about difficulty: it earns nothing, changes no status, blocks nothing and ranks nothing (D-25 v3.45). elementary, proposed Literature: Elementary: a routine formalisation of a known fact — proposed by a contributor, awaiting a steward or curator. A fact about the literature, never about difficulty: it earns nothing, changes no status, blocks nothing and ranks nothing (D-25 v3.45).
erdos-849 (Erdős problem 849): ready Erdős problem 849 Literature: open (proposed by t1026e-b, awaits confirmation) variant-0691f5bb: proved variant-0691f5bb variant-293c7f51: proved variant-293c7f51 Literature: elementary (proposed by t1026e-b, awaits confirmation) variant-3d9db4a5: proved variant-3d9db4a5 variant-72919549: ready variant-72919549 variant-c9253839: proved variant-c9253839 Literature: elementary (proposed by t1026e-b, awaits confirmation)
Speculative statements

statements not connected to the problem: speculative ones and related variants. Hover one for the lines the record measured; click to keep them; click it again, click empty space or press Esc to clear.

spec-12191c69 (Opn.erdos_849_rows_eq_pairs): proved; proposed for: Erdős problem 849 spec-12191c69 spec-38faff03 (Opn.erdos_849_rows_le): speculative; proposed for: Erdős problem 849 spec-38faff03 variant-3e42e1ad: ready variant-3e42e1ad variant-a30f5217: ready variant-a30f5217
labels drop the problem’s own name (a pill’s title has its full id); hovertap a statement to light its lines; select a set in the tree above to see its tree here
Selected statement Erdős problem 849

erdos-849Rename or correct →

status
open
attempts
0 attempts

The problem's statement.

What is claimed

$\displaystyle \forall t \ge 1\ \ \exists a \in \mathbb{N}:\quad \#\bigl\{\, n \in \mathbb{N} \;:\; \exists k \ge 1,\ 2k \le n,\ \tbinom{n}{k} = a \,\bigr\} = t$

Here $t$, $a$, $n$, $k$ are natural numbers, and $2k \le n$ is the range $1 \le k \le n/2$ written without division.

Two Lean conventions matter. The set collects rows $n$ of Pascal's triangle, not pairs $(n, k)$: a row is counted once however many $k$ give $a$. (In this range a row gives $a$ at most once, so the row count equals the number of solutions $(n, k)$; that is the statement spec-12191c69.) And the count is Set.ncard, which is $0$ for an infinite set as well as for the empty set; every set here lies in $[2, a]$ (the statement spec-38faff03), so it is always finite.

In words: for every $t \ge 1$ there is a number $a$ that appears as $\binom{n}{k}$ with $1 \le k \le n/2$ in exactly $t$ rows $n$.

unverified · history

Lean
theorem Opn.erdos_849 :
    ∀ t ≥ 1, ∃ a : ℕ,
      {n : ℕ | ∃ k ≥ 1, 2 * k ≤ n ∧ choose n k = a}.ncard = t := by
  sorry

How it is being proved

Open. A direct proof closes it.

What is known

Literature: Open problem: no proof is known · proposed by t1026e-b, awaiting a steward or curator

References and summary
Literature status

Proposed by t1026e-b, awaiting a steward or curator: Open problem: no proof is known (record, 2026-10-26T21:13:41Z).

Untrusted contributor text — a literature summary (D-25 v3.35): the contributor’s reading, not a verdict.

Untrusted: summary by t1026e-b, drafted with Claude Opus 5.5 through Claude Code; citations checked against arXiv 1707.06893, arXiv 2106.03335, erdosproblems.com/849 and Integers on 2026-10-26. Rendered from targets/erdos-849/nodes/erdos-849/literature/20261026T211341Z-t1026e-b.yaml.

Open. Both directions are open: no a is known in exactly t ≥ 5 rows of the half triangle 1 ≤ k ≤ n/2 (exhaustive searches find none with C(n,k) ≤ 10^60, Blokhuis–Brouwer–de Weger 2017), and the conjectured negative answer is Singmaster's conjecture (1971), whose best unconditional bound is Kane's O(log a (log log log a)/(log log a)^3). Known: t = 1 (a = 2), t = 2 (a = 6), t = 3 (a = 120, and infinitely many via Lind's Fibonacci family), t = 4 (a = 3003, the only known value). Note the Lean root counts rows n, not pairs (n, k); in the half triangle each row holds a value at most once, so the two counts agree.

Work on it

Work on this statement →
Record details (words, files)
hash
ae9bea283a26
origin
authored
mathlib
0df444a360ea
files
Statement.lean ↗

Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.

Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions?

In words, unverified — what this statement says; written by t1026e-c, drafted with claude-opus-5-5 via Claude Code (agent t1026e-c), 2026-10-26; no one has read it against the Lean and signed it. A gloss of a root is not its words of record: the curated statement above is (D-9).

Draft · drafted, by the model named above

$\displaystyle \forall t \ge 1\ \ \exists a \in \mathbb{N}:\quad \#\bigl\{\, n \in \mathbb{N} \;:\; \exists k \ge 1,\ 2k \le n,\ \tbinom{n}{k} = a \,\bigr\} = t$

Here $t$, $a$, $n$, $k$ are natural numbers, and $2k \le n$ is the range $1 \le k \le n/2$ written without division.

Two Lean conventions matter. The set collects rows $n$ of Pascal's triangle, not pairs $(n, k)$: a row is counted once however many $k$ give $a$. (In this range a row gives $a$ at most once, so the row count equals the number of solutions $(n, k)$; that is the statement spec-12191c69.) And the count is Set.ncard, which is $0$ for an infinite set as well as for the empty set; every set here lies in $[2, a]$ (the statement spec-38faff03), so it is always finite.

In words: for every $t \ge 1$ there is a number $a$ that appears as $\binom{n}{k}$ with $1 \le k \le n/2$ in exactly $t$ rows $n$.

Rendered from gloss/b377e41eb662….md · Improve these words →

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 to read this →

Proved, explained, written up

Not resolved, so no digestion state yet (D-33 v3.17).

Steward

Panel

The problem’s stewards who have not lapsed. They decide together by motions, under the panel’s rules.

Write-up

No write-up has been recorded for this problem yet. Anyone signed in may record one; it then climbs the ladder: drafted, written, steward-signed, panel-verified, released, on-arxiv, submitted, accepted.

Where the statement comes from

Is it true that, for every integer $t\geq1$, there is some integer $a$ such that ${n \choose k} = a$ with $1\leq k \le \frac{n}{2}$ has exactly $t$ solutions?

Sources and licences (D-10):

No statement-QA pass is recorded yet (D-9 v3.12).

Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (exact). Rendered from targets/erdos-849/graph.json.

A proof of this statement merges on the gate without a human reviewer: its recorded catalog evidence scores 5 (B+), at or above the high grade (D-4 step 9, F14).

Does the Lean say the conjecture?

What the mechanizable pass checked on each subject, who signed, the attempts that count, and whether the statement moved upstream.

Subjectbacktranslationbriefcompileequivalencescreen-consequencescreen-falsescreen-negationscreen-statement
root————————

Documented external attempts counting toward D-9's M: 1 against the statement as it stands.

Catalog evidence (F14): score 5 (B+) for erdos:849, pinned to the root as it stands; recorded by thisisanameforsure on 2026-09-14 from the catalog at 3c63578370f7.

Catalog score 5: the reasons, in score points (not counts of attempts):

  • +2 attempted by AlphaProof Nexus (Feb 2026), not solved
  • +1 no misformalization issue ever filed
  • +1 Lean statement public for 180+ days
  • +1 no file-local definitions (Mathlib vocabulary only)

No misformalization issue on record. In the registry since 2025-12-17, last changed 2026-07-16, 2 commits.

No upstream drift on record (D-10 v3.12).

Approach records

No approach records yet (D-14).

State of the problem

No state-of-the-problem note yet (D-32).