Erdős problem 493 · problems.science

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$ ?

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

493.lean

Retained formal statement1 of 1

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.

FormalConjectures/ErdosProblems/493.leanErdos493.erdos_4931 lineExact file

1True ↔ ∃ k N, ∀ (n : ℤ), N ≤ n → ∃ a, (∀ (i : Fin k), 2 ≤ a i) ∧ ∏ i, a i - ∑ i, a i = 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.

Sources

Search problems.science