Is it true that if $1 \leq a_{1} < a_{2} < \dots$ is a sequence of integers with $lim inf a_{n}^{1/ 2^{n}} > 1$ then $n = 1 \sum \infty \frac{1}{a _{n} a _{n + 1}}$ is irrational?

Worked, still open.

irrationality · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

This is **not known in general**. It’s an old conjecture of **Erdős**.

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

AMS 11 · solved (literature)

theorem erdos_1051 :
    answer(True) ↔ ∀ (a : ℕ → ℤ), StrictMono a → GrowthCondition a →
      Irrational (ErdosSeries a)

solved