Erdős problem 435 · problems.science

Let $n\in\mathbb{N}$ with $n\neq p^k$ for any prime $p$ and $k\geq 0$ . What is the largest integer not of the form $\sum_{1\leq i<n}c_i\binom{n}{i}$ where the $c_i\geq 0$ are integers?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/435.lean

Formal Conjectures

FormalConjectures/ErdosProblems/435.leanErdos435.erdos_4355 linesExact file

1∀ (n : ℕ),2  n ≠ 0 →3    (∀ (p k : ℕ), Nat.Prime p → n ≠ p ^ k) →4      IsGreatest {m | ¬∃ c, m = ∑ i ∈ Finset.Ico 1 n, ↑(c i) * ↑(n.choose i)}5        (∑ 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.

Proof manifests naming this Problem

Jayyhk Erdős Leanjayyhk:erdos:435
PLBY Lean proofsErdosProblems.Erdos435

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Formalization
Erdős AI contributions wiki · 4 Feb, 2026
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science