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?

Sources

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

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

351.lean

Retained formal statement1 of 3

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?

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.

Search problems.science

Find a Problem, Result, source, or page