Let $a_{1} < a_{2} < \dots$ be an increasing sequence such that $a_{n} / n \to \infty$ . Is the sum $n \sum \frac{a _{n}}{2 ^{a_{n}}}$ irrational?

Worked, still open.

irrationality · open · 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 is recorded as **Erdős Problem #260** and is still listed as **open** (the problem page was last edited **19 October 2025**). ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_260 : answer(sorry) ↔
                  ∀ a : ℕ → ℤ, ∀ s : ℝ,
                  StrictMono a →
                  Tendsto (fun n => (a n : ℝ ) / n ) atTop atTop →
                  HasSum (fun n => (a n : ℝ ) / 2 ^ a n) s → Irrational s

formal-conjectures/260.lean ↗

status

open

evidence

formal

status

Search Vela