Skip to content

Erdős problem 346

Let A={1a1<a2<}A=\{1\leq a_1< a_2<\cdots\} be a set of integers such that A\BA\backslash B is complete for any finite subset BB and not complete for any infinite subset BB. If an+1/an1+ϵa_{n+1}/a_n \geq 1+\epsilon for all nn, must limnan+1/an=(1+5)/2\lim_n a_{n+1}/a_n=(1+\sqrt{5})/2? Under the reading where the ratio limit is assumed to exist, a Lean-verified argument forces the limit to be the golden ratio; a separate construction disproves the literal statement where convergence is not assumed.

Sources

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

7 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

346.lean

Retained formal statement5 of 6

The sequence f is not complete whenever infinitely many terms are removed from it, and this is proved in [Gr64d].

FormalConjectures/ErdosProblems/346.leanErdos346.erdos_346.variants.f_not_isAddComplete1 lineExact file
∀ {B : Set ℕ}, BSet.range Erdos346.fB.Infinite → ¬IsAddComplete (Set.range Erdos346.f \ B)
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page