Skip to content

Erdős problem 351

Let p(x)∈Q[x]p(x) \in \mathbb{Q}[x] be a non-constant rational polynomial with positive leading coefficient. Is it true that A={p(n)+1/n:n∈N}A=\{ p(n)+1/n : n \in \mathbb{N}\} is strongly complete, in the sense that, for any finite set BB, {∑a∈Xa:X⊆A∖B,X is finite}\left\{\sum_{a \in X} a : X \subseteq A \setminus B, X \textrm{ is finite}\right\} contains all sufficiently large integers?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/351.lean

Formal Conjectures

FormalConjectures/ErdosProblems/351.leanErdos351.erdos_3511 lineExact file
True ↔ ∀ (P : Polynomial ℚ), 0 < P.natDegree → 0 < P.leadingCoeff → Erdos351.HasCompleteImage P
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:351
  • PLBY Lean proofsErdosProblems.Erdos351

Reported activity

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

  • Formalization

    Erdős AI contributions wiki · 6 May, 2026

    Machine
    Claude Opus 4.7, GPT-5.5 Pro
    Open the source record

  • AI collaborating with humans

    Erdős AI contributions wiki · 3 May, 2026

    Machine
    GPT-5.5 Pro
    People
    Kevin Barreto, Liam Price
    Open the source record

  • argument

    VibeMathed

    Machine
    GPT-5.5 Pro
    People
    Kevin Barreto, Liam Price
    Reported outcome
    resolved
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page