Skip to content

Erdős problem 1051

Is it true that if a0<a1<a2<⋯a_0 < a_1 < a_2 < \cdots is a strictly increasing sequence of integers with lim inf⁡an1/2n>1\liminf a_n^{1/2^n} > 1, then the series ∑n=0∞1an⋅an+1\sum_{n=0}^\infty \frac{1}{a_n \cdot a_{n+1}} is irrational?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/1051.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1051.leanErdos1051.erdos_10511 lineExact file
True ↔ ∀ (a : ℕ → ℤ), StrictMono a → Erdos1051.GrowthCondition a → Irrational (Erdos1051.ErdosSeries a)
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:1051
  • PLBY Lean proofsErdosProblems.Erdos1051

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page