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 statement1 of 6

Is it true that for every lacunary, strongly complete sequence A that is not complete whenever infinitely many terms are removed from it, lim A (n + 1) / A n = (1 + √5) / 2?

FormalConjectures/ErdosProblems/346.leanErdos346.erdos_3466 linesExact file
True  ∀ {A : ℕ → ℕ},    IsLacunary A      IsAddStronglyCompleteNatSeq A        (∀ BSet.range A, B.Infinite → ¬IsAddComplete (Set.range A \ B)) →          Filter.Tendsto (fun n => ↑(A (n + 1)) / ↑(A n)) Filter.atTop (nhds ((1 + √5) / 2))
OpenStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page