FormalConjectures/ErdosProblems/493.lean

GitHub source file

1 declarations, 1 contain sorry, 0 declared as axioms

1. theorem Erdos493.erdos_493 Does there exist a $k$ such that every sufficiently large integer can be written in the form $$\prod_{i=1}^k a_i - \sum_{i=1}^k a_i$$ for some integers $a_i\geq 2$? sorry line 40 source

   Source documentation

   Does there exist a $k$ such that every sufficiently large integer can be written in the form $$\prod_{i=1}^k a_i - \sum_{i=1}^k a_i$$ for some integers $a_i\geq 2$?

   Erdős attributes this question to Schinzel. Eli Seamans has observed that the answer is yes (with $k=2$) for a very simple reason: $n = 2(n+2)-(2+(n+2))$. There may well have been some additional constraint in the problem as Schinzel posed it, but [Er61] does not record what this is.

   depends on sorry what this means

   Statement uses: Iff, True, Exists, Nat, Int, LE.le, Fin, And, OfNat.ofNat, Eq, HSub.hSub, Finset.prod, Finset.univ, Finset.sum

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

   15 instances, coercions and auxiliary constants left out.

   Tactic trace: 1 steps

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

   theorem erdos_493 : answer(True) ↔
       ∃ k : ℕ, ∃ N : ℤ, ∀ n : ℤ, N ≤ n →
         ∃ a : Fin k → ℤ,
           (∀ i : Fin k, (2 : ℤ) ≤ a i) ∧
           (∏ i : Fin k, a i) - (∑ i : Fin k, a i) = n := by
   …