Erdős problem 264 · problems.science

Kovač and Tao [KoTa24] generally proved that any strictly increasing sequence of positive integers $a_n$ such that $\sum \frac{1}{a_n}$ converges and $\liminf_{n \to \infty} (a_n^2 \sum_{k > n} \frac{1}{a_k^2}) > 0$ is not an irrationality sequence.

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/264.lean

Formal Conjectures

FormalConjectures/ErdosProblems/264.leanErdos264.erdos_264.parts.i1 lineExact file

1¬Erdos264.IsIrrationalitySequence fun x => 2 ^ x

SolvedStatement only, no proofformal statement reference

Proof manifests naming this Problem

PLBY Lean proofsErdosProblems.Erdos264
PLBY Lean proofsErdosProblems.Erdos264b

Reported activity

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

AI building on literature
Erdős AI contributions wiki · 18 Dec, 2025
Machine
Aristotle
Open the source record

Continue

Start a contribution Browse the source files Open the collection entry

No current result

Proof manifests naming this Problem

Reported activity

Continue

Search problems.science