Skip to content

Erdős problem 435

Let n∈Nn\in\mathbb{N} with n≠pkn\neq p^k for any prime pp and k≥0k\geq 0. What is the largest integer not of the form ∑1≤i<nci(ni)\sum_{1\leq i<n}c_i\binom{n}{i} where the ci≥0c_i\geq 0 are integers?

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

435.lean

Retained formal statement1 of 1

Let n∈Nn\in\mathbb{N} with n≠pkn\neq p^k for any prime pp and k≥0k\geq 0. What is the largest integer not of the form ∑1≤i<nci(ni)\sum_{1\leq i<n}c_i\binom{n}{i} where the ci≥0c_i\geq 0 are integers?

If n=∏pkakn=\prod p_k^{a_k} then the largest integer not of this form is ∑k(∑1≤d≤ak(npkd))(pk−1)−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 p → n ≠ p ^ k) →      IsGreatest {m | ¬∃ c, m = ∑ i ∈ Finset.Ico 1 n, ↑(c i) * ↑(n.choose i)}        (∑ p ∈ n.primeFactors, (∑ d ∈ Finset.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.