Skip to content

Erdős problem 493

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

Sources

The source's own material, retained exactly.

1 retained statement36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

493.lean

Retained formal statement1 of 1

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

Erdős attributes this question to Schinzel. Eli Seamans has observed that the answer is yes (with k=2k=2) for a very simple reason: n=2(n+2)−(2+(n+2))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
True ↔ ∃ 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.