Skip to content

Problems · Vela Mathematics Program

Narrowed toformalized ×complete sequences ×Clear all

Problem ledger

5 problemsGraph view
declared open · formalizederdos:346
Let A={1≤a1<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/an≥1+ϵa_{n+1}/a_n \geq 1+\epsilon for all nn, must lim⁡nan+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.
number theorycomplete sequencesN/A4 sources
declared proved (Lean) · formalizederdos:347
True ↔ ∃ a, Monotone a ∧ Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 2) ∧ ∀ (ι : ℕ → ℕ), (Set.range ι)ᶜ.Finite → (subsetSums (Set.range (a ∘ ι))).HasDensity 1
number theorycomplete sequencesN/A6 sources
declared open · formalizederdos:348
{x | ∃ m n, ∃ (_ : m < n), ∃ a, ∃ (_ : Monotone a) (_ : ∀ (s : Finset ℕ), s.card = m → IsAddComplete (Set.range (Function.updateFinset a s 0))) (_ : ∀ (t : Finset ℕ), t.card = n → ¬IsAddComplete (Set.range (Function.updateFinset a t 0))), (m, n) = x} = sorry
number theorycomplete sequencesN/A2 sources
declared open · formalizederdos:349
∀ (t α : ℝ), 0 < t → 2 < α → ¬Erdos349.IsGoodPair t α
number theorycomplete sequencesN/A3 sources
declared proved (Lean) · formalizederdos:351
True ↔ ∀ (P : Polynomial ℚ), 0 < P.natDegree → 0 < P.leadingCoeff → Erdos351.HasCompleteImage P
number theorycomplete sequencesN/A6 sources

Search problems.science

Find a Problem, Result, source, or page