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

Erdős and Graham [ErGr80] remark that it is easy to see that if A (n + 1) / A n > (1 + √5) / 2 then the second property is automatically satisfied.

FormalConjectures/ErdosProblems/346.leanErdos346.erdos_346.variants.gt_goldenRatio_not_IsAddComplete3 linesExact file
∀ {A : ℕ → ℕ},  (∀ (n : ℕ), (1 + √5) / 2 * ↑(A n) < ↑(A (n + 1))) →    ∀ {B : Set ℕ}, BSet.range AB.Infinite → ¬IsAddComplete (Set.range A \ B)
SolvedStatement only, no proof

Search problems.science

Find a Problem, Result, source, or page