Number theory

Erdős 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?

References

erdosproblems.com/849

No one has attempted this yet.

Formal statement

Lean type

True ↔ ∀ t ≥ 1, ∃ a, {n | ∃ k ≥ 1, 2 * k ≤ n ∧ n.choose k = a}.ncard = t

What you must prove

import FormalConjectures.ErdosProblems.«849»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos849.erdos_849" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/849.lean

Source type SHA-256: sha256:1fd73d95d2ff39aa91222466c0987e9ab168b2f0984eae65161211a49e91dd56
Task id: fc-379fc029-erdos849-erdos-849-9e4dcae01a-formalized-v1
Task commitment: sha256:842c1c8de9e853ce9d7a8eea252bc54bdda42344b3ac9326a7e730549508a67c

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.