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=1kaii=1kai\prod_{i=1}^k a_i - \sum_{i=1}^k a_i for some integers ai2a_i\geq 2?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/493.lean

Formal Conjectures

FormalConjectures/ErdosProblems/493.leanErdos493.erdos_4931 lineExact file
True ↔ ∃ k N, ∀ (n : ℤ), Nn → ∃ 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:493
  • PLBY Lean proofsErdosProblems.Erdos493

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI building on literature

    Erdős AI contributions wiki · 2025

    Machine
    Aristotle, GPT, Seed Prover
    Open the source record

Continue

Search problems.science

Find a Problem, Result, source, or page