FormalConjectures/ErdosProblems/435.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

1. theorem Erdos435.erdos_435 Let $n\in\mathbb{N}$ with $n\neq p^k$ for any prime $p$ and $k\geq 0$ sorry line 47 source

   Source documentation

   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?

   If $n=\prod p_k^{a_k}$ then the largest integer not of this form is $$\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.

   depends on sorry what this means

   Statement uses: Nat, Ne, OfNat.ofNat, Nat.Prime, HPow.hPow, IsGreatest, Int, Set.ofPred, Not, Exists, Eq, Finset.sum, Finset.Ico, HMul.hMul, Nat.choose, HSub.hSub, Nat.primeFactors, Finset.Icc, Finsupp, Nat.factorization

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   40 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

   Open to load the checked before-and-after goal states.

   theorem erdos_435 (n : ℕ) (hn : n ≠ 0)
       (hpk : ∀ p k : ℕ, p.Prime → 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) := by
   …

   Mentions: c