Erdős problem 435
Let with for any prime and . What is the largest integer not of the form where the are integers?
Sources
FormalConjectures/ErdosProblems/
435.lean
Retained formal statement
Let with for any prime and . What is the largest integer not of the form where the are integers?
If then the largest integer not of this form is This was first proved by Hwang and Song [HwSo24]. Independently this was found in the comment section by Peake and Cambie.
∀ (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)