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

Erdős and Graham [ErGr80] also say that it is not hard to construct very irregular sequences satisfying the aforementioned properties.

FormalConjectures/ErdosProblems/346.leanErdos346.erdos_346.variants.example5 linesExact file
A,  IsAddStronglyCompleteNatSeq A    (∀ BSet.range A, B.Infinite → ¬IsAddComplete (Set.range A \ B)) ∧      Filter.liminf (fun n => ↑(A (n + 1)) / 2) Filter.atTop = 1 ∧        Filter.limsup (fun n => ↑(A (n + 1)) / ↑(A n)) Filter.atTop = ⊤
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page