Skip to content

Erdős problem 435

Let nNn\in\mathbb{N} with npkn\neq p^k for any prime pp and k0k\geq 0. What is the largest integer not of the form 1i<nci(ni)\sum_{1\leq i<n}c_i\binom{n}{i} where the ci0c_i\geq 0 are integers?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

435.lean

Retained formal statement1 of 1

Let nNn\in\mathbb{N} with npkn\neq p^k for any prime pp and k0k\geq 0. What is the largest integer not of the form 1i<nci(ni)\sum_{1\leq i<n}c_i\binom{n}{i} where the ci0c_i\geq 0 are integers?

If n=pkakn=\prod p_k^{a_k} then the largest integer not of this form is k(1dak(npkd))(pk1)n.\sum_k \left( \sum_{1\leq d\leq a_k}\binom{n}{p_k^d}\right)(p_k-1)-n. This was first proved by Hwang and Song [HwSo24]. Independently this was found in the comment section by Peake and Cambie.

FormalConjectures/ErdosProblems/435.leanErdos435.erdos_4355 linesExact file
∀ (n : ℕ),  n ≠ 0 →    (∀ (p k : ℕ), Nat.Prime pnp ^ k) →      IsGreatest {m | ¬∃ c, m = ∑ iFinset.Ico 1 n, ↑(c i) * ↑(n.choose i)}        (∑ pn.primeFactors, (∑ dFinset.Icc 1 (n.factorization p), ↑(n.choose (p ^ d))) * (↑p - 1) - ↑n)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Search problems.science

Find a Problem, Result, source, or page