Is it true that there are only finitely many pairs of intervals $I_{1}, I_{2}$ such that $n_{1} \in I_{1} \sum \frac{1}{n _{1}} + n_{2} \in I_{2} \sum \frac{1}{n _{2}} \in N ?$

Worked, still open.

number theory · 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’s an **open problem** of Erdős and Graham.

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

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

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_288 : answer(sorry) ↔ Set.Finite { I : Fin 2 → ℕ+ × ℕ+ |
    ∀ j, (I j).1 ≤ (I j).2 ∧
      ∃ n : ℕ+, (∑ j : Fin 2, ∑ nⱼ ∈ Set.Icc (I j).1 (I j).2, (nⱼ⁻¹ : ℚ)) = n }

formal-conjectures/288.lean ↗

status

open

evidence

formal

status

Search Vela